From a193cc0fe1f6d7dbe37b96a9e2abcebf07c959e3 Mon Sep 17 00:00:00 2001 From: ZhangQixiang123 Date: Wed, 27 Aug 2025 10:50:31 +0800 Subject: [PATCH 01/10] inductive type definition: core and value implemented --- .../__tests__/test_doEliminator_core.ts | 290 ++++++++++++++++++ src/pie_interpreter/evaluator/evaluator.ts | 59 ++++ .../typechecker/synthesizer.ts | 111 +++++-- src/pie_interpreter/typechecker/utils.ts | 3 +- src/pie_interpreter/types/core.ts | 88 +++++- src/pie_interpreter/types/neutral.ts | 25 ++ src/pie_interpreter/types/source.ts | 86 ++++++ src/pie_interpreter/types/utils.ts | 12 + src/pie_interpreter/types/value.ts | 50 ++- 9 files changed, 689 insertions(+), 35 deletions(-) create mode 100644 src/pie_interpreter/__tests__/test_doEliminator_core.ts diff --git a/src/pie_interpreter/__tests__/test_doEliminator_core.ts b/src/pie_interpreter/__tests__/test_doEliminator_core.ts new file mode 100644 index 00000000..f814313d --- /dev/null +++ b/src/pie_interpreter/__tests__/test_doEliminator_core.ts @@ -0,0 +1,290 @@ +import 'jest'; +import * as C from '../types/core'; +import * as V from '../types/value'; +import * as Evaluator from '../evaluator/evaluator'; +import { Environment } from '../utils/environment'; +import { inspect } from 'util'; +import { readBack } from '../evaluator/utils'; +import { Context } from '../utils/context'; + +// Test examples for doEliminator function using Core data structures + +// Example 1: List elimination test +export function createListExample(): { + listType: C.InductiveType, + sampleList: C.Core, + eliminator: C.Eliminator +} { + + const listType = new C.InductiveType( + "List", + [new C.Nat()], // parameters + [], // no indices + ); + + // Create List constructors + const nilConstructor = new C.Constructor( + "List", + listType, // type: List A + [], // no arguments + 0, // constructor index + [] + ); + + // Create a sample list: cons 1 (cons 2 (cons 3 nil)) + // Create cons 3 nil + const cons3Nil = new C.Constructor( + "List", + listType, + [ + new C.Add1(new C.Add1(new C.Add1(new C.Zero()))), + nilConstructor + ], + 1, + [nilConstructor] + ); + + // Create cons 2 (cons 3 nil) + const cons2 = new C.Constructor( + "List", + listType, + [new C.Add1(new C.Add1(new C.Zero())), cons3Nil], // 2, (cons 3 nil) + 1, + [cons3Nil] + ); + + + // Create eliminator for summing the list with proper lambda expressions + const sumEliminator = new C.Eliminator( + "List", + cons2, + new C.Lambda("xs", new C.Nat()), // motive: List A -> Nat + [ + new C.Zero(), // base case: nil -> 0 + new C.Lambda("head", + new C.Lambda("tail", + new C.Lambda( + 'n', + new C.Add1(new C.VarName('n')) + ) + ) + ) // step case: head -> tail -> sum_tail -> add1 sum_tail + ] + ); + + return { + listType, + sampleList: cons2, + eliminator: sumEliminator + }; +} + +// // Example 2: Binary Tree elimination test +// export function createBinaryTreeExample(): { +// treeType: C.InductiveType, +// sampleTree: C.Core, +// eliminator: C.Eliminator +// } { + +// // Create Tree constructors +// const leafConstructor = new C.Constructor( +// "leaf", +// new C.VarName("Tree"), // type: Tree A +// [], // no arguments +// 0, // constructor index +// false // not recursive +// ); + +// const nodeConstructor = new C.Constructor( +// "node", +// new C.Pi("value", new C.VarName("A"), +// new C.Pi("left", new C.VarName("Tree"), +// new C.Pi("right", new C.VarName("Tree"), +// new C.VarName("Tree")))), // type: A -> Tree A -> Tree A -> Tree A +// [], // no arguments for constructor schema +// 1, // constructor index +// true // recursive (contains Tree A) +// ); + +// // Create the Tree inductive type +// const treeType = new C.InductiveType( +// "Tree", +// [new C.VarName("A")], // parameters +// [], // no indices +// [leafConstructor, nodeConstructor], +// new C.Eliminator("Tree", +// new C.VarName("tree"), // target +// new C.VarName("P"), // motive +// [ +// new C.VarName("base_leaf"), // method for leaf +// new C.VarName("step_node") // method for node +// ] +// ) +// ); + +// // Create a sample tree: node 5 (node 3 leaf (node 4 leaf leaf)) (node 7 leaf leaf) + +// // Create leaf instances +// const leaf1 = new C.Constructor("leaf", new C.VarName("Tree"), [], 0, false); +// const leaf2 = new C.Constructor("leaf", new C.VarName("Tree"), [], 0, false); +// const leaf3 = new C.Constructor("leaf", new C.VarName("Tree"), [], 0, false); +// const leaf4 = new C.Constructor("leaf", new C.VarName("Tree"), [], 0, false); + +// // Create node 4 leaf leaf +// const node4 = new C.Constructor( +// "node", +// new C.VarName("Tree"), +// [ +// new C.Add1(new C.Add1(new C.Add1(new C.Add1(new C.Zero())))), // 4 +// leaf1, +// leaf2 +// ], +// 1, +// true +// ); + +// // Create node 3 leaf (node 4 leaf leaf) +// const node3 = new C.Constructor( +// "node", +// new C.VarName("Tree"), +// [ +// new C.Add1(new C.Add1(new C.Add1(new C.Zero()))), // 3 +// leaf3, +// node4 +// ], +// 1, +// true +// ); + +// // Create node 7 leaf leaf +// const node7 = new C.Constructor( +// "node", +// new C.VarName("Tree"), +// [ +// new C.Add1(new C.Add1(new C.Add1(new C.Add1(new C.Add1(new C.Add1(new C.Add1(new C.Zero()))))))), // 7 +// leaf4, +// new C.Constructor("leaf", new C.VarName("Tree"), [], 0, false) +// ], +// 1, +// true +// ); + +// // Create root node 5 (node 3 ...) (node 7 ...) +// const sampleTree = new C.Constructor( +// "node", +// new C.VarName("Tree"), +// [ +// new C.Add1(new C.Add1(new C.Add1(new C.Add1(new C.Add1(new C.Zero()))))), // 5 +// node3, +// node7 +// ], +// 1, +// true +// ); + +// // Create eliminator for summing tree values +// const sumEliminator = new C.Eliminator( +// "Tree", +// sampleTree, +// new C.Lambda("tree", new C.Nat()), // motive: always Nat +// [ +// new C.Zero(), // base case: leaf -> 0 +// new C.Lambda("value", +// new C.Lambda("left", +// new C.Lambda("right", +// new C.Lambda("left_sum", +// new C.Lambda("right_sum", +// new C.Application( // value + (left_sum + right_sum) +// new C.Application( +// new C.VarName("+"), +// new C.VarName("value") +// ), +// new C.Application( +// new C.Application( +// new C.VarName("+"), +// new C.VarName("left_sum") +// ), +// new C.VarName("right_sum") +// ) +// ) +// ) +// ) +// ) +// ) +// ) // step case: value -> left -> right -> left_sum -> right_sum -> value + left_sum + right_sum +// ] +// ); + +// return { +// treeType, +// sampleTree, +// eliminator: sumEliminator +// }; +// } + +// Jest test cases +describe("doEliminator tests", () => { + + it("should handle list elimination", () => { + const env: Environment = new Map(); + const listExample = createListExample(); + + expect(() => { + const listResult = Evaluator.doEliminator( + "List", + listExample.sampleList.toLazy(env), + listExample.eliminator.motive.toLazy(env), + listExample.eliminator.methods.map(m => m.toLazy(env)) + ); + const context: Context = new Map(); + const normalizedResult = readBack(context, new V.Nat(), listResult); + console.log("List elimination result (normalized):", inspect(normalizedResult, true, null, true)); + }).not.toThrow(); + }); + + // it("should handle binary tree elimination", () => { + + // const env: Environment = new Map(); + // const treeExample = createBinaryTreeExample(); + + // expect(() => { + // const treeResult = Evaluator.doEliminator( + // "Tree", + // treeExample.sampleTree.toLazy(env), + // treeExample.eliminator.motive.toLazy(env), + // treeExample.eliminator.methods.map(m => m.toLazy(env)) + // ); + // console.log("Tree elimination result:", treeResult); + // }).not.toThrow(); + // }); + + it("should test list elimination with specific values", () => { + const env: Environment = new Map(); + const listExample = createListExample(); + + const listResult = Evaluator.doEliminator( + "List", + listExample.sampleList.toLazy(env), + listExample.eliminator.motive.toLazy(env), + listExample.eliminator.methods.map(m => m.toLazy(env)) + ); + + // Add specific assertions based on expected behavior + expect(listResult).toBeDefined(); + }); + + // it("should test tree elimination with specific values", () => { + // const env: Environment = new Map(); + // const treeExample = createBinaryTreeExample(); + + // const treeResult = Evaluator.doEliminator( + // "Tree", + // treeExample.sampleTree.toLazy(env), + // treeExample.eliminator.motive.toLazy(env), + // treeExample.eliminator.methods.map(m => m.toLazy(env)) + // ); + + // // Add specific assertions based on expected behavior + // expect(treeResult).toBeDefined(); + // }); +}); \ No newline at end of file diff --git a/src/pie_interpreter/evaluator/evaluator.ts b/src/pie_interpreter/evaluator/evaluator.ts index 8fb70c3f..d9f1013b 100644 --- a/src/pie_interpreter/evaluator/evaluator.ts +++ b/src/pie_interpreter/evaluator/evaluator.ts @@ -775,4 +775,63 @@ export function doIndEither(target: V.Value, motive: V.Value, left: V.Value, rig } } throw new Error(`invalid input for indEither: ${[target, motive, left, right]}`); +} + +export function doEliminator(name: string, target: V.Value, motive: V.Value, methods: V.Value[]): V.Value { + const targetNow = target.now(); + + // Check if target is a constructor application of the inductive type + if (targetNow instanceof V.Constructor) { + if (targetNow.name != name) { + throw new Error(`doEliminator: wrong eliminator used. Got: ${targetNow.name}; Expected: ${name}`); + } + const constructorIndex = targetNow.index; + if (constructorIndex >= 0 && constructorIndex < methods.length) { + const method = methods[constructorIndex]; + let result = method; + + // Apply method to constructor arguments + // Pattern: apply all non-recursive arguments first, then recursive arguments with their inductive hypotheses + for (let i = 0; i < targetNow.args.length; i++) { + const arg = targetNow.args[i]; + result = doApp(result, arg); + } + + for (let i = 0; i < targetNow.recursive_args.length; i++) { + const arg = targetNow.recursive_args[i]; + const recursiveResult = doEliminator(name, arg, motive, methods); + result = doApp(result, recursiveResult); + } + + return result; + } + } else if (targetNow instanceof V.Neutral) { + const typeNow = targetNow.type.now(); + if (typeNow instanceof V.InductiveType && typeNow.name === name) { + // Create neutral eliminator application + return new V.Neutral( + doApp(motive, target), + new N.GenericEliminator( + name, + targetNow.neutral, + new N.Norm( + new V.Pi( + "x", + typeNow, + new HigherOrderClosure((_) => new V.Universe()) + ), + motive + ), + methods.map((method, i) => + new N.Norm( + typeNow, + method + ) + ) + ) + ); + } + } + + throw new Error(`doEliminator: invalid input for ${name}: ${[target, motive, methods]}`); } \ No newline at end of file diff --git a/src/pie_interpreter/typechecker/synthesizer.ts b/src/pie_interpreter/typechecker/synthesizer.ts index 5995f18f..788b47f6 100644 --- a/src/pie_interpreter/typechecker/synthesizer.ts +++ b/src/pie_interpreter/typechecker/synthesizer.ts @@ -30,16 +30,16 @@ export class synthesizer { ); } - public static synthArrow(context: Context, r: Renaming, location: Location, arg1 : S.Source, arg2 : S.Source, args : S.Source[]): Perhaps { + public static synthArrow(context: Context, r: Renaming, location: Location, arg1: S.Source, arg2: S.Source, args: S.Source[]): Perhaps { if (args.length === 0) { const z = freshBinder(context, arg2, 'x'); const Aout = new PerhapsM("Aout"); const Bout = new PerhapsM('Bout'); return goOn( [ - [Aout, () => + [Aout, () => arg1.check(context, r, new V.Universe())], - [Bout, () => + [Bout, () => arg2.check( bindFree(context, z, valInContext(context, Aout.value)), r, @@ -68,11 +68,11 @@ export class synthesizer { [Aout, () => arg1.check(context, r, new V.Universe())], [tout, () => new S.Arrow(notForInfo(location), arg2, first, rest) - .check( - bindFree(context, z, valInContext(context, Aout.value)), - r, - new V.Universe() - ) + .check( + bindFree(context, z, valInContext(context, Aout.value)), + r, + new V.Universe() + ) ] ], () => { @@ -316,7 +316,7 @@ export class synthesizer { return goOn( [ [tgtout, () => target.check(context, r, new V.Nat())], - [motout, () => motive.check(context, r, + [motout, () => motive.check(context, r, new V.Pi( 'n', new V.Nat(), @@ -384,12 +384,12 @@ export class synthesizer { return goOn( [ [Aout, () => first.check(context, r, new V.Universe())], - [Dout, () => + [Dout, () => second.check( bindFree(context, a, valInContext(context, Aout.value)), r, new V.Universe() - )], + )], ], () => new go( new C.The( @@ -446,7 +446,7 @@ export class synthesizer { return goOn( [ [Aout, () => type.check(context, r, new V.Universe())], - [Dout, () => + [Dout, () => new S.Sigma( notForInfo(location), rest, @@ -564,7 +564,7 @@ export class synthesizer { ) } - public static synthIndList(context: Context, r: Renaming, + public static synthIndList(context: Context, r: Renaming, location: Location, target: S.Source, motive: S.Source, base: S.Source, step: S.Source,): Perhaps { const tgtout = new PerhapsM('tgtout'); const motout = new PerhapsM('motout'); @@ -583,7 +583,7 @@ export class synthesizer { return goOn( [ [ - motout, + motout, () => motive.check( context, r, @@ -654,7 +654,7 @@ export class synthesizer { } - public static synthRecList(context: Context, r: Renaming, + public static synthRecList(context: Context, r: Renaming, location: Location, target: S.Source, base: S.Source, step: S.Source,): Perhaps { const tgtout = new PerhapsM('tgtout'); return goOn( @@ -671,7 +671,7 @@ export class synthesizer { [ [bout, () => base.synth(context, r)], [btval, () => new go(valInContext(context, bout.value.type))], - [sout, () => + [sout, () => step.check( context, r, @@ -742,7 +742,7 @@ export class synthesizer { return goOn( [ [fstout, () => x.synth(context, r)], - [restout, () => + [restout, () => xs.check( context, r, @@ -1014,7 +1014,7 @@ export class synthesizer { const [Av, fromv, tov] = [result.type, result.from, result.to]; return goOn( [ - [motout, () => + [motout, () => motive.check( context, r, @@ -1034,7 +1034,7 @@ export class synthesizer { ) ], [motv, () => new go(valInContext(context, motout.value))], - [baseout, () => + [baseout, () => base.check( context, r, @@ -1157,7 +1157,7 @@ export class synthesizer { } public static synthIndVec(context: Context, r: Renaming, location: Location, - length: S.Source, target: S.Source, motive: S.Source, base: S.Source, step: S.Source): Perhaps { + length: S.Source, target: S.Source, motive: S.Source, base: S.Source, step: S.Source): Perhaps { const lenout = new PerhapsM('lenout'); const lenv = new PerhapsM('lenv'); const vecout = new PerhapsM('vecout'); @@ -1255,7 +1255,7 @@ export class synthesizer { public static synthIndEither(context: Context, r: Renaming, location: Location, target: S.Source, - motive: S.Source, baseLeft: S.Source, baseRight: S.Source,): Perhaps { + motive: S.Source, baseLeft: S.Source, baseRight: S.Source,): Perhaps { const tgtout = new PerhapsM('tgtout'); const motout = new PerhapsM('motout'); const motval = new PerhapsM('motval'); @@ -1269,7 +1269,7 @@ export class synthesizer { const [Lv, Rv] = [result.leftType, result.rightType]; return goOn( [ - [motout, () => + [motout, () => motive.check( context, r, @@ -1360,7 +1360,7 @@ export class synthesizer { const argout = new PerhapsM('argout'); return goOn( [[argout, () => arg.check(context, r, A)]], - () => + () => new go( new C.The( c.valOfClosure(valInContext(context, argout.value)).readBackType(context), @@ -1489,4 +1489,69 @@ export class synthesizer { ); } } + + public static synthDefineDatatype( + ctx: Context, + renames: Renaming, + datatype: S.DefineDatatype + ): Perhaps { + + let checkAndBuildTypes = (initialType: V.Value, binder: TypedBinder[]): Perhaps => { + let normalizedType = [] + for (const param of binder) { + const paramCheck = param.type.check(ctx, renames, new V.Universe()); + if (paramCheck instanceof stop) return paramCheck; + normalizedType.push((paramCheck as go).result); + } + + let cur_Type = initialType + for (let i = normalizedType.length - 1; i >= 0; i--) { + const paramType = normalizedType[i]; + const paramName = binder[i].findNames(); + const currentTType = cur_Type; + cur_Type = new V.Pi( + paramName, + valInContext(ctx, paramType), + new HigherOrderClosure((v: V.Value) => currentTType) + ); + } + + return new go(cur_Type); + + } + + const normalizedResultTypeTemp = datatype.resultType.check(ctx, renames, new V.Universe()); + + if (normalizedResultTypeTemp instanceof stop) return normalizedResultTypeTemp; + + const normalizedIndicesTemp = checkAndBuildTypes( + (normalizedResultTypeTemp as go).result, datatype.indices); + + if (normalizedIndicesTemp instanceof stop) return normalizedIndicesTemp; + + const normalizedParametersTemp = + checkAndBuildTypes((normalizedIndicesTemp as go).result, datatype.parameters); + + let normalizedConstructor: V.Value[] = [] + + for (const constructor of datatype.constructors) { + const normalizedResultType = (constructor as S.Constructor).resultType.check(ctx, renames, new V.Universe()); + if (normalizedResultType instanceof stop) return normalizedResultType; + const normalizedConstructorTypeTemp = checkAndBuildTypes( + (normalizedResultType as go).result, + constructor.args + ); + + if (normalizedConstructorTypeTemp instanceof stop) return normalizedConstructorTypeTemp; + + normalizedConstructor.push((normalizedConstructorTypeTemp as go).result); + } + + + + + + } + + } \ No newline at end of file diff --git a/src/pie_interpreter/typechecker/utils.ts b/src/pie_interpreter/typechecker/utils.ts index 316723e2..e956c01c 100644 --- a/src/pie_interpreter/typechecker/utils.ts +++ b/src/pie_interpreter/typechecker/utils.ts @@ -96,4 +96,5 @@ function isAlphabetic(char: string): boolean { // Helper to concoct a function application form in source syntax export function makeApp(a: Source, b: Source, cs: Source[]): Source { return new Application(a.location, a, b, cs); -} \ No newline at end of file +} + diff --git a/src/pie_interpreter/types/core.ts b/src/pie_interpreter/types/core.ts index cf6cf729..3dfe5c03 100644 --- a/src/pie_interpreter/types/core.ts +++ b/src/pie_interpreter/types/core.ts @@ -2,7 +2,7 @@ import * as V from "./value"; import * as N from './neutral'; import * as Evaluator from '../evaluator/evaluator'; -import { Environment, getValueFromEnvironment} from '../utils/environment'; +import { Environment, getValueFromEnvironment } from '../utils/environment'; import { SourceLocation } from '../utils/locations'; import { FirstOrderClosure, isVarName } from './utils'; @@ -254,7 +254,7 @@ export class Pi extends Core { public valOf(env: Environment): V.Value { const typeVal = this.type.toLazy(env); - return new V.Pi(this.name, typeVal, + return new V.Pi(this.name, typeVal, new FirstOrderClosure(env, this.name, this.body) ); } @@ -278,7 +278,7 @@ export class Lambda extends Core { ) { super() } public valOf(env: Environment): V.Value { - return new V.Lambda(this.param, + return new V.Lambda(this.param, new FirstOrderClosure(env, this.param, this.body)); } @@ -337,7 +337,7 @@ export class Sigma extends Core { public valOf(env: Environment): V.Value { const typeVal = this.type.toLazy(env); - return new V.Sigma(this.name, typeVal, + return new V.Sigma(this.name, typeVal, new FirstOrderClosure(env, this.name, this.body)); } @@ -534,7 +534,7 @@ export class IndList extends Core { } export class Trivial extends Core { - + public valOf(env: Environment): V.Value { return new V.Trivial(); } @@ -626,7 +626,7 @@ export class Equal extends Core { public prettyPrint(): string { return `(= ${this.type.prettyPrint()} ${this.left.prettyPrint()} - ${this.right.prettyPrint()})`; + ${this.right.prettyPrint()})`; } public toString(): string { @@ -754,7 +754,7 @@ export class Symm extends Core { } export class IndEqual extends Core { - + constructor( public target: Core, public motive: Core, @@ -789,7 +789,7 @@ export class Vec extends Core { public valOf(env: Environment): V.Value { return new V.Vec( - this.type.toLazy(env), + this.type.toLazy(env), this.length.toLazy(env) ); } @@ -937,7 +937,7 @@ export class Either extends Core { public toString(): string { return this.prettyPrint(); } - + } export class Left extends Core { @@ -1080,4 +1080,72 @@ export class VarName extends Core { return this.prettyPrint(); } -} \ No newline at end of file +} + +export class InductiveType extends Core { + public valOf(env: Environment): V.Value { + return new V.InductiveType( + this.typeName, + this.parameters.map(p => p.toLazy(env)), + this.indices.map(i => i.toLazy(env)), + ); + } + constructor( + public typeName: string, + public parameters: Core[], + public indices: Core[], + ) { super(); } + + public prettyPrint(): string { + return `${this.typeName}${this.parameters.length > 0 ? ' ' + this.parameters.map(p => p.prettyPrint()).join(' ') : ''}${this.indices.length > 0 ? ' ' + this.indices.map(i => i.prettyPrint()).join(' ') : ''}`; + } +} + +export class Constructor extends Core { + + constructor( + public name: string, + public type: Core, + public args: Core[], + public index: number, + public recursive_args: Core[] + ) { super(); } + + public valOf(env: Environment): V.Value { + return new V.Constructor( + this.name, + this.type.toLazy(env), + this.args.map(a => a.toLazy(env)), + this.index, + this.recursive_args.map(a => a.toLazy(env)) + ) + } + + public prettyPrint(): string { + const args = this.args.map(a => a.prettyPrint()).join(' '); + return `(${this.name}${args.length > 0 ? ' ' + args : ''})`; + } +} + +export class Eliminator extends Core { + + constructor( + public typeName: string, + public target: Core, + public motive: Core, + public methods: Core[] + ) { super(); } + + public valOf(env: Environment): V.Value { + return Evaluator.doEliminator( + this.typeName, + this.target.toLazy(env), + this.motive.toLazy(env), + this.methods.map(m => m.toLazy(env)) + ); + } + public prettyPrint(): string { + const methods = this.methods.map(m => m.prettyPrint()).join(' '); + return `(elim-${this.typeName} ${this.target.prettyPrint()} ${this.motive.prettyPrint()} ${methods})`; + } +} diff --git a/src/pie_interpreter/types/neutral.ts b/src/pie_interpreter/types/neutral.ts index c567acdb..63f6e3ef 100644 --- a/src/pie_interpreter/types/neutral.ts +++ b/src/pie_interpreter/types/neutral.ts @@ -517,6 +517,31 @@ export class IndEither extends Neutral { } } +export class GenericEliminator extends Neutral { + + constructor( + public typeName: string, + public target: Neutral, + public motive: Norm, + public methods: Norm[] + ) { + super(); + } + + public readBackNeutral(context: Context): C.Core { + return new C.Eliminator( + this.typeName, + this.target.readBackNeutral(context), + readBack(context, this.motive.type, this.motive.value), + this.methods.map(method => readBack(context, method.type, method.value)) + ); + } + + public prettyPrint() { + return `N-GenericEliminator-${this.typeName}`; + } +} + export class Application extends Neutral { constructor(public operator: Neutral, public operand: Norm) { diff --git a/src/pie_interpreter/types/source.ts b/src/pie_interpreter/types/source.ts index fbfbbc0a..073363a3 100644 --- a/src/pie_interpreter/types/source.ts +++ b/src/pie_interpreter/types/source.ts @@ -1947,4 +1947,90 @@ export class Application extends Source { public toString(): string { return this.prettyPrint(); } +} + +export class DefineDatatype extends Source { + constructor( + public location: Location, + public typeName: string, + public parameters: TypedBinder[], // Type parameters [A : Type] + public indices: TypedBinder[], // Index parameters [i : Nat] + public resultType: Source, // The result universe (Type) + public constructors: Constructor[] // Data constructors + ) { super(location); } + + protected synthHelper(ctx: Context, renames: Renaming): Perhaps { + return Synth.synthDefineDatatype(ctx, renames, this); + } + + public findNames(): string[] { + const names = [this.typeName]; + names.push(...this.parameters.flatMap(p => p.findNames())); + names.push(...this.indices.flatMap(i => i.findNames())); + names.push(...this.resultType.findNames()); + names.push(...this.constructors.flatMap(c => c.findNames())); + return names; + } + + public prettyPrint(): string { + const params = this.parameters.map(p => `[${p.prettyPrint()}]`).join(' '); + const indices = this.indices.map(i => `[${i.prettyPrint()}]`).join(' '); + const ctors = this.constructors.map(c => c.prettyPrint()).join('\n '); + return `(define-datatype ${this.typeName} ${params} : ${indices} ${this.resultType.prettyPrint()} + ${ctors})`; + } +} + +export class Constructor extends Source { + protected synthHelper(ctx: Context, renames: Renaming): Perhaps { + throw new Error('Method not implemented.'); + } + constructor( + public location: Location, + public name: string, + public args: TypedBinder[], // Constructor args + public resultType: Source // Type the constructor produces + ) { + super(location); + } + + public findNames(): string[] { + const names = [this.name]; + names.push(...this.args.flatMap(a => a.findNames())); + names.push(...this.resultType.findNames()); + return names; + } + + public prettyPrint(): string { + const args = this.args.map(a => `[${a.prettyPrint()}]`).join(' '); + return `[${this.name} ${args} : ${this.resultType.prettyPrint()}]`; + } +} + +// Generic eliminator for user-defined inductive types +export class GenericEliminator extends Source { + constructor( + public location: Location, + public typeName: string, + public target: Source, + public motive: Source, + public methods: Source[] + ) { super(location); } + + protected synthHelper(ctx: Context, renames: Renaming): Perhaps { + throw new Error('Method not implemented.'); + } + + public findNames(): string[] { + const names = [this.typeName]; + names.push(...this.target.findNames()); + names.push(...this.motive.findNames()); + names.push(...this.methods.flatMap(m => m.findNames())); + return names; + } + + public prettyPrint(): string { + const methods = this.methods.map(m => m.prettyPrint()).join(' '); + return `(elim-${this.typeName} ${this.target.prettyPrint()} ${this.motive.prettyPrint()} ${methods})`; + } } \ No newline at end of file diff --git a/src/pie_interpreter/types/utils.ts b/src/pie_interpreter/types/utils.ts index 6f878c4d..860580e9 100644 --- a/src/pie_interpreter/types/utils.ts +++ b/src/pie_interpreter/types/utils.ts @@ -14,6 +14,10 @@ export class SiteBinder { public location: Location, public varName: string, ) { } + + public prettyPrint(): string { + return `${this.varName}`; + } } // Define TypedBinder, which is a SiteBinder associated with a expression in Pie. @@ -23,6 +27,14 @@ export class TypedBinder { public binder: SiteBinder, public type: Source, ) {} + + public prettyPrint(): string { + return `${this.binder.prettyPrint()} : ${this.type.prettyPrint()}`; + } + + public findNames(): string { + return this.binder.varName; + } } export function isPieKeywords(str : string) : boolean { diff --git a/src/pie_interpreter/types/value.ts b/src/pie_interpreter/types/value.ts index ac428f86..333f4679 100644 --- a/src/pie_interpreter/types/value.ts +++ b/src/pie_interpreter/types/value.ts @@ -621,4 +621,52 @@ export class Absurd extends Value { return this.prettyPrint(); } -} \ No newline at end of file +} + +export class InductiveType extends Value { + constructor( + public name: string, + public parameters: Value[], + public indices: Value[], + ) { super() } + + public readBackType(context: Context): C.Core { + return new C.InductiveType( + this.name, + this.parameters.map(p => p.readBackType(context)), + this.indices.map(i => i.readBackType(context)), + ) + } + + public prettyPrint(): string { + return `InductiveType ${this.name}`; + } + + public toString(): string { + return this.prettyPrint(); + } +} + +export class Constructor extends Value { + + constructor( + public name: string, + public type: Value, + public args: Value[], + public index: number, + public recursive_args: Value[], + ) { super() } + + public readBackType(context: Context): C.Core { + throw new Error("No readBackType for Constructor."); + } + + public prettyPrint(): string { + const args = this.args.map(a => a.prettyPrint()).join(' '); + return `(${this.name}${args.length > 0 ? ' ' + args : ''})`; + } + + public toString(): string { + return this.prettyPrint(); + } +} From da0063b439d7dad1843a50d0383ba0bba374699e Mon Sep 17 00:00:00 2001 From: ZhangQixiang123 Date: Wed, 3 Sep 2025 14:34:13 +0800 Subject: [PATCH 02/10] inductive datatype constructor generation(temp) --- .../__tests__/test_doEliminator_core.ts | 6 +- .../__tests__/test_inductive_design.ts | 245 ++++++++++++++++++ .../typechecker/definedatatype.ts | 124 +++++++++ .../typechecker/synthesizer.ts | 197 +++++++++++--- src/pie_interpreter/types/core.ts | 51 +++- src/pie_interpreter/types/source.ts | 49 +++- src/pie_interpreter/types/value.ts | 42 ++- src/pie_interpreter/utils/context.ts | 35 ++- 8 files changed, 695 insertions(+), 54 deletions(-) create mode 100644 src/pie_interpreter/__tests__/test_inductive_design.ts create mode 100644 src/pie_interpreter/typechecker/definedatatype.ts diff --git a/src/pie_interpreter/__tests__/test_doEliminator_core.ts b/src/pie_interpreter/__tests__/test_doEliminator_core.ts index f814313d..6e9646f9 100644 --- a/src/pie_interpreter/__tests__/test_doEliminator_core.ts +++ b/src/pie_interpreter/__tests__/test_doEliminator_core.ts @@ -25,7 +25,7 @@ export function createListExample(): { // Create List constructors const nilConstructor = new C.Constructor( "List", - listType, // type: List A + "List", // type: List A [], // no arguments 0, // constructor index [] @@ -35,7 +35,7 @@ export function createListExample(): { // Create cons 3 nil const cons3Nil = new C.Constructor( "List", - listType, + "List", [ new C.Add1(new C.Add1(new C.Add1(new C.Zero()))), nilConstructor @@ -47,7 +47,7 @@ export function createListExample(): { // Create cons 2 (cons 3 nil) const cons2 = new C.Constructor( "List", - listType, + "List", [new C.Add1(new C.Add1(new C.Zero())), cons3Nil], // 2, (cons 3 nil) 1, [cons3Nil] diff --git a/src/pie_interpreter/__tests__/test_inductive_design.ts b/src/pie_interpreter/__tests__/test_inductive_design.ts new file mode 100644 index 00000000..d7e5f923 --- /dev/null +++ b/src/pie_interpreter/__tests__/test_inductive_design.ts @@ -0,0 +1,245 @@ +import 'jest'; +import * as S from '../types/source'; +import { TypedBinder, SiteBinder } from '../types/utils'; +import { Location, Syntax } from '../utils/locations'; +import { Position } from '../../scheme_parser/transpiler/types/location'; + +// Test location +const testLoc = new Location(new Syntax(new Position(1, 1), new Position(1, 1), 'test'), false); + +describe("Inductive Types Design Test", () => { + + it("should demonstrate ConstructorType vs Constructor distinction", () => { + + // ============================================ + // STEP 1: Define List datatype using ConstructorType + // ============================================ + + const listDatatype = new S.DefineDatatype( + testLoc, + "List", + // Parameters: [A : Type] + [new TypedBinder(new SiteBinder(testLoc, "A"), new S.Universe(testLoc))], + // Indices: (none) + [], + // Result type: Type + new S.Universe(testLoc), + // Constructors: ConstructorType[] (just signatures) + [ + // nil : List A + new S.ConstructorType( + testLoc, + "nil", + [], // no arguments + new S.Application( + testLoc, + new S.Name(testLoc, "List"), + new S.Name(testLoc, "A"), + [] + ) + ), + + // cons : A -> List A -> List A + new S.ConstructorType( + testLoc, + "cons", + [ + new TypedBinder(new SiteBinder(testLoc, "head"), new S.Name(testLoc, "A")), + new TypedBinder(new SiteBinder(testLoc, "tail"), + new S.Application(testLoc, new S.Name(testLoc, "List"), new S.Name(testLoc, "A"), []) + ) + ], + new S.Application(testLoc, new S.Name(testLoc, "List"), new S.Name(testLoc, "A"), []) + ) + ] + ); + + // ============================================ + // STEP 2: Use Constructor for actual constructor calls + // ============================================ + + // nil (no arguments) + const nilExpr = new S.Constructor( + testLoc, + "nil", + [], // no actual arguments + listDatatype + ); + + // cons 42 nil + const cons42Nil = new S.Constructor( + testLoc, + "cons", + [ + new S.Number(testLoc, 42), // head argument + nilExpr // tail argument + ], + listDatatype + ); + + // cons 1 (cons 42 nil) + const nestedList = new S.Constructor( + testLoc, + "cons", + [ + new S.Number(testLoc, 1), // head + cons42Nil // tail + ], + listDatatype + ); + + // ============================================ + // STEP 3: Eliminator usage + // ============================================ + + const listLength = new S.GenericEliminator( + testLoc, + "List", + nestedList, // target: our nested list + // motive: List A -> Nat + new S.Lambda( + testLoc, + [new SiteBinder(testLoc, "xs")], + new S.Nat(testLoc) + ), + // methods: [nil-case, cons-case] + [ + // nil case: 0 + new S.Zero(testLoc), + + // cons case: λ head tail length_of_tail. add1 length_of_tail + new S.Lambda( + testLoc, + [ + new SiteBinder(testLoc, "head"), + new SiteBinder(testLoc, "tail"), + new SiteBinder(testLoc, "length_of_tail") + ], + new S.Add1(testLoc, new S.Name(testLoc, "length_of_tail")) + ) + ] + ); + + // ============================================ + // STEP 4: Test the structure + // ============================================ + + // Test datatype definition structure + expect(listDatatype.typeName).toBe("List"); + expect(listDatatype.constructors).toHaveLength(2); + + // Test constructor types (in definition) + const nilCtorType = listDatatype.constructors[0]; + const consCtorType = listDatatype.constructors[1]; + + expect(nilCtorType).toBeInstanceOf(S.ConstructorType); + expect(nilCtorType.name).toBe("nil"); + expect(nilCtorType.args).toHaveLength(0); + + expect(consCtorType).toBeInstanceOf(S.ConstructorType); + expect(consCtorType.name).toBe("cons"); + expect(consCtorType.args).toHaveLength(2); + expect(consCtorType.args[0].binder.varName).toBe("head"); + expect(consCtorType.args[1].binder.varName).toBe("tail"); + + // Test constructor applications (in expressions) + expect(nilExpr).toBeInstanceOf(S.Constructor); + expect(nilExpr.name).toBe("nil"); + expect(nilExpr.args).toHaveLength(0); + + expect(cons42Nil).toBeInstanceOf(S.Constructor); + expect(cons42Nil.name).toBe("cons"); + expect(cons42Nil.args).toHaveLength(2); + expect(cons42Nil.args[0]).toBeInstanceOf(S.Number); + expect(cons42Nil.args[1]).toBeInstanceOf(S.Constructor); // nested constructor + + // Test eliminator structure + expect(listLength).toBeInstanceOf(S.GenericEliminator); + expect(listLength.typeName).toBe("List"); + expect(listLength.target).toBeInstanceOf(S.Constructor); + expect(listLength.methods).toHaveLength(2); + + console.log("✅ Design structure is correct!"); + console.log("ConstructorType used in definitions:", nilCtorType.constructor.name); + console.log("Constructor used in expressions:", nilExpr.constructor.name); + }); + + // it("should demonstrate Vector with indices", () => { + + // // Vec A n datatype + // const vecDatatype = new S.DefineDatatype( + // testLoc, + // "Vec", + // [new TypedBinder(new SiteBinder(testLoc, "A"), new S.Universe(testLoc))], // parameters + // [new TypedBinder(new SiteBinder(testLoc, "n"), new S.Nat(testLoc))], // indices + // new S.Universe(testLoc), + // [ + // // vnil : Vec A zero + // new S.ConstructorType( + // testLoc, + // "vnil", + // [], + // new S.Application( + // testLoc, + // new S.Name(testLoc, "Vec"), + // new S.Name(testLoc, "A"), + // [new S.Zero(testLoc)] + // ) + // ), + + // // vcons : (n : Nat) -> A -> Vec A n -> Vec A (add1 n) + // new S.ConstructorType( + // testLoc, + // "vcons", + // [ + // new TypedBinder(new SiteBinder(testLoc, "n"), new S.Nat(testLoc)), + // new TypedBinder(new SiteBinder(testLoc, "head"), new S.Name(testLoc, "A")), + // new TypedBinder(new SiteBinder(testLoc, "tail"), + // new S.Application(testLoc, new S.Name(testLoc, "Vec"), new S.Name(testLoc, "A"), [new S.Name(testLoc, "n")]) + // ) + // ], + // new S.Application( + // testLoc, + // new S.Name(testLoc, "Vec"), + // new S.Name(testLoc, "A"), + // [new S.Add1(testLoc, new S.Name(testLoc, "n"))] + // ) + // ) + // ] + // ); + + // // Using constructors: vcons 2 'a' (vcons 1 'b' (vcons 0 'c' vnil)) + // const vnil = new S.Constructor(testLoc, "vnil", []); + + // const vec1 = new S.Constructor( + // testLoc, + // "vcons", + // [ + // new S.Zero(testLoc), // n = 0 + // new S.Quote(testLoc, "c"), // head = 'c' + // vnil // tail = vnil + // ] + // ); + + // const vec2 = new S.Constructor( + // testLoc, + // "vcons", + // [ + // new S.Add1(testLoc, new S.Zero(testLoc)), // n = 1 + // new S.Quote(testLoc, "b"), // head = 'b' + // vec1 // tail = previous vec + // ] + // ); + + // // Test indexed structure + // expect(vecDatatype.indices).toHaveLength(1); + // expect(vecDatatype.indices[0].binder.varName).toBe("n"); + + // const vconsType = vecDatatype.constructors[1]; + // expect(vconsType.args).toHaveLength(3); // n, head, tail + // expect(vconsType.args[0].binder.varName).toBe("n"); + + // console.log("✅ Indexed Vec structure is correct!"); + // }); + +}); \ No newline at end of file diff --git a/src/pie_interpreter/typechecker/definedatatype.ts b/src/pie_interpreter/typechecker/definedatatype.ts new file mode 100644 index 00000000..4e68b96e --- /dev/null +++ b/src/pie_interpreter/typechecker/definedatatype.ts @@ -0,0 +1,124 @@ +import * as S from '../types/source'; +import * as C from '../types/core'; +import * as V from '../types/value'; +import { go, goOn, Perhaps, stop } from '../types/utils'; +import { Context, extendContext, getInductiveType, InductiveDatatypePlaceholder, InductiveDatatypeBinder, ConstructorBinder, contextToEnvironment } from '../utils/context'; +import { Location } from '../utils/locations'; +import { rename, Renaming } from './utils'; +import { Constructor } from '../types/value'; +import { Environment } from '../utils/environment'; + +export class DefineDatatypeSource { + constructor( + public location: Location, + public name: string, + public parameters: S.The[], + public indices: S.The[], + public constructors: { name: string, args: S.The[] }[], + public typeValue: V.Value + ) { } + + public toString(): string { + return `data ${this.name} ${this.parameters.map(p => p.toString()).join(' ')} where ${this.constructors.map(c => c.name + ' ' + c.args.map(a => a.toString()).join(' ')).join(', ')}`; + } + + public typeSynth(ctx: Context, rename: Renaming): Perhaps { + const synthedParameters = this.parameters.map(p => p.type.isType(ctx, rename)) + .map(p => { + if (p instanceof stop) { + throw new Error(`Parameter type is not a type at ${p.where}`) + } + return (p as go).result + }) + const synthedIndices = this.indices.map(p => p.type.isType(ctx, rename)) + .map(p => { + if (p instanceof stop) { + throw new Error(`Index type is not a type at ${p.where}`) + } + return (p as go).result + }) + let counter = 0 + const synthedConstructors = this.constructors.map( + p => { + let rec_args: S.InductiveTypeInfo[] = [] + counter += 1 + const typecheckedArgs = p.args.map( + arg => { + if (arg.type instanceof S.InductiveTypeInfo) { + if (arg.type.name === this.name) { + rec_args = [...rec_args, arg.type] + return arg.type.isType(ctx, rename) + } +//TODO: Probably this else is negligible, becuase we need to add check inductive type in isType + else { + const inductiveTypeTemp = getInductiveType(ctx, arg.location, arg.type.name) + if (inductiveTypeTemp instanceof stop) { + throw new Error(`No inductive type found for ${arg.type.name} at ${arg.location}`) + } + return new go((inductiveTypeTemp as go).result.type.readBackType(ctx)) + } + } else { + return arg.type.isType(ctx, rename) + } + } + ).map(p => { + if (p instanceof stop) { + throw new Error(`Constructor argument type is not a type at ${p.where}`) + } + return (p as go).result + }) + const coreRecArgs = rec_args.map(recArg => recArg.isType(ctx, rename)) + .map(p => { + if (p instanceof stop) { + throw new Error(`Recursive argument type is not a type at ${p.where}`) + } + return (p as go).result + }) + return new C.Constructor(p.name, this.name, typecheckedArgs, counter, coreRecArgs) + } + ) + return new go(new DefineDatatypeCore(this.name, synthedParameters, synthedIndices, synthedConstructors)) + } + + +} + +export class DefineDatatypeCore { + constructor( + public name: string, + public parameters: C.Core[], + public indices: C.Core[], + public constructors: C.Constructor[] + ) { } + + public valOf(env: Environment): V.InductiveType { + return new V.InductiveType( + this.name, + this.parameters.map(p => p.toLazy(env)), + this.indices.map(i => i.toLazy(env)), +) } +} + +export function handleDefineDatatype(ctx: Context, renaming: Renaming, target: DefineDatatypeSource): Perhaps { + const placeholder = new InductiveDatatypePlaceholder(target.name) + if (ctx.has(target.name)) { + throw new Error(`this name is already in use ${target.name}`) + } + extendContext(ctx, target.name, placeholder) + + const synthesized = target.typeSynth(ctx, renaming) + if (synthesized instanceof stop) { + return synthesized + } + + const core = (synthesized as go).result + ctx.delete(target.name) + + extendContext(ctx, core.name, new InductiveDatatypeBinder(core.name, core.valOf(contextToEnvironment(ctx)))) + + for (const ctor of core.constructors) { + extendContext(ctx, ctor.name, new ConstructorBinder(ctor.name, ctor.valOf(contextToEnvironment(ctx)))) + } + + return new go(ctx) +} \ No newline at end of file diff --git a/src/pie_interpreter/typechecker/synthesizer.ts b/src/pie_interpreter/typechecker/synthesizer.ts index 788b47f6..e065e17b 100644 --- a/src/pie_interpreter/typechecker/synthesizer.ts +++ b/src/pie_interpreter/typechecker/synthesizer.ts @@ -13,6 +13,8 @@ import { notForInfo } from "../utils/locations"; import { doApp, doCar, indVecStepType } from "../evaluator/evaluator"; import { readBack } from '../evaluator/utils'; import { Location } from '../utils/locations'; +import { ConstructorType, DefineDatatype } from '../types/source'; +import { alphaEquiv } from "../utils/alphaeqv"; export class synthesizer { @@ -1490,68 +1492,181 @@ export class synthesizer { } } - public static synthDefineDatatype( + public static synthDataType(context: Context, r: Renaming, datatype: S.DefineDatatype): Perhaps { + + } + + public static GenerateConstructor( ctx: Context, renames: Renaming, datatype: S.DefineDatatype ): Perhaps { - let checkAndBuildTypes = (initialType: V.Value, binder: TypedBinder[]): Perhaps => { - let normalizedType = [] - for (const param of binder) { - const paramCheck = param.type.check(ctx, renames, new V.Universe()); - if (paramCheck instanceof stop) return paramCheck; - normalizedType.push((paramCheck as go).result); + let buildConstructorApplication = (constructorName: string, argNames: string[], datatypeName: string, parameters: C.Core[], indices: C.Core[]): C.Core => { + let result: C.Core = new C.VarName(datatypeName); + + // Apply parameters + for (const param of parameters) { + result = new C.Application(result, param); } - - let cur_Type = initialType - for (let i = normalizedType.length - 1; i >= 0; i--) { - const paramType = normalizedType[i]; - const paramName = binder[i].findNames(); - const currentTType = cur_Type; - cur_Type = new V.Pi( - paramName, - valInContext(ctx, paramType), - new HigherOrderClosure((v: V.Value) => currentTType) + + // Apply indices + for (const index of indices) { + result = new C.Application(result, index); + } + + // Apply constructor + let constructorApp: C.Core = new C.VarName(constructorName); + for (const argName of argNames) { + constructorApp = new C.Application(constructorApp, new C.VarName(argName)); + } + + return constructorApp; + }; + + let generateMethodType = ( + constructorName: string, + argTypes: C.Core[], + rec_args: C.Core[], + resultType: C.Core, + motive: C.Core, + datatypeName: string, + parameters: C.Core[], + indices: C.Core[] + ): C.Core => { + let argNames: string[] = []; + let recArgNames: string[] = []; + + // Generate argument names + for (let i = 0; i < argTypes.length; i++) { + argNames.push(fresh(ctx, `arg_${i}`)); + } + + // Generate inductive hypothesis names + for (let i = 0; i < rec_args.length; i++) { + recArgNames.push(fresh(ctx, `ih_${i}`)); + } + + // Build the constructor application + const constructorApp = buildConstructorApplication(constructorName, argNames, datatypeName, parameters, indices); + + // Final result type: motive applied to constructor application + let methodType: C.Core = new C.Application(motive, constructorApp); + + // Add inductive hypotheses (right to left) + for (let i = rec_args.length - 1; i >= 0; i--) { + const ihName = recArgNames[i]; + const recArgApp = new C.Application(motive, new C.VarName(argNames[i])); // Apply motive to recursive argument + + methodType = new C.Pi( + ihName, + recArgApp, + methodType ); } + + // Add constructor arguments (right to left) + for (let i = argTypes.length - 1; i >= 0; i--) { + const argName = argNames[i]; + methodType = new C.Pi( + argName, + argTypes[i], + methodType + ); + } + + return methodType; + }; + const resultType = new PerhapsM('resultType'); + const parameters = new PerhapsM('parameters'); + const indices = new PerhapsM('indices'); + const constructorTypes = new PerhapsM('constructorTypes'); + const eliminatorTypes = new PerhapsM('eliminatorTypes'); - return new go(cur_Type); - - } - - const normalizedResultTypeTemp = datatype.resultType.check(ctx, renames, new V.Universe()); - - if (normalizedResultTypeTemp instanceof stop) return normalizedResultTypeTemp; + return goOn( + [ + [resultType, () => datatype.resultType.check(ctx, renames, new V.Universe())], + [parameters, () => datatype.parameters.map((param) => param.type.check(ctx, renames, new V.Universe()))], + [indices, () => datatype.indices.map((index) => index.type.check(ctx, renames, new V.Universe()))], + [constructorTypes, () => datatype.constructors.map((constructor) => this.checkConstructorType(ctx, renames, constructor as S.ConstructorType))], + [eliminatorTypes, () => { + const resultTypeResult = resultType.value; + const parametersResults = parameters.value; + const indicesResults = indices.value; + const constructorTypesResults = constructorTypes.value; + const motiveType = new C.Pi( + 'test_input_fst', + resultTypeResult, + new C.Universe() + ) - const normalizedIndicesTemp = checkAndBuildTypes( - (normalizedResultTypeTemp as go).result, datatype.indices); + - if (normalizedIndicesTemp instanceof stop) return normalizedIndicesTemp; - const normalizedParametersTemp = - checkAndBuildTypes((normalizedIndicesTemp as go).result, datatype.parameters); + }] + ], + () => new go( + new C.The( + new C.Universe(), + new C.InductiveType( + datatype.typeName, + parameters.value, + indices.value + ) + ) + ) + ); - let normalizedConstructor: V.Value[] = [] + } - for (const constructor of datatype.constructors) { - const normalizedResultType = (constructor as S.Constructor).resultType.check(ctx, renames, new V.Universe()); - if (normalizedResultType instanceof stop) return normalizedResultType; - const normalizedConstructorTypeTemp = checkAndBuildTypes( - (normalizedResultType as go).result, - constructor.args - ); + public static checkConstructorType(ctx: Context, renames: Renaming, ConstructorType: S.ConstructorType): Perhaps { + const normalizedResultTypeTemp = ConstructorType.resultType.check(ctx, renames, new V.Universe()); - if (normalizedConstructorTypeTemp instanceof stop) return normalizedConstructorTypeTemp; + let binder = ConstructorType.args; - normalizedConstructor.push((normalizedConstructorTypeTemp as go).result); + let normalizedType = [] + for (const param of binder) { + const paramCheck = param.type.check(ctx, renames, new V.Universe()); + if (paramCheck instanceof stop) return paramCheck; + normalizedType.push((paramCheck as go).result); } + let recur_args = [] + let normalizedResultType = (normalizedResultTypeTemp as go).result + for (const arg of normalizedType) { + if (alphaEquiv(arg, normalizedResultType)) { + recur_args.push(arg); + } + } - - + return new go(new C.ConstructorType( + normalizedType, + recur_args, + (normalizedResultTypeTemp as go).result + )); + } +} + +function checkAndBuildTypes(ctx: Context, renames: Renaming, initialType: C.Core, binder: TypedBinder[]): Perhaps { + let normalizedType = [] + for (const param of binder) { + const paramCheck = param.type.check(ctx, renames, new V.Universe()); + if (paramCheck instanceof stop) return paramCheck; + normalizedType.push((paramCheck as go).result); } + let cur_Type = initialType + for (let i = normalizedType.length - 1; i >= 0; i--) { + const paramType = normalizedType[i]; + const paramName = binder[i].findNames(); + const currentTType = cur_Type; + cur_Type = new V.Pi( + paramName, + valInContext(ctx, paramType), + new HigherOrderClosure((v: V.Value) => currentTType) + ); + } + return new go(cur_Type); } \ No newline at end of file diff --git a/src/pie_interpreter/types/core.ts b/src/pie_interpreter/types/core.ts index 3dfe5c03..f38c7436 100644 --- a/src/pie_interpreter/types/core.ts +++ b/src/pie_interpreter/types/core.ts @@ -1094,6 +1094,8 @@ export class InductiveType extends Core { public typeName: string, public parameters: Core[], public indices: Core[], + public constructorTypes: Core[], + public eliminatorType: Core[] ) { super(); } public prettyPrint(): string { @@ -1105,16 +1107,16 @@ export class Constructor extends Core { constructor( public name: string, - public type: Core, + public type: string, public args: Core[], public index: number, public recursive_args: Core[] ) { super(); } - public valOf(env: Environment): V.Value { + public valOf(env: Environment): V.Constructor { return new V.Constructor( this.name, - this.type.toLazy(env), + this.type, this.args.map(a => a.toLazy(env)), this.index, this.recursive_args.map(a => a.toLazy(env)) @@ -1127,6 +1129,26 @@ export class Constructor extends Core { } } +export class ConstructorType extends Core { + + constructor( + public argTypes: The[], + public rec_args: Core[], + public resultType: Core + ) { super(); } + + public valOf(env: Environment): V.Value { + return new V.ConstructorType( + this.argTypes.map(a => a.toLazy(env)), + this.resultType.toLazy(env) + ); + } + + public prettyPrint(): string { + return `ConstructorType ${this.argTypes.map(a => a.prettyPrint()).join(' ')} ${this.resultType.prettyPrint()}`; + } +} + export class Eliminator extends Core { constructor( @@ -1149,3 +1171,26 @@ export class Eliminator extends Core { return `(elim-${this.typeName} ${this.target.prettyPrint()} ${this.motive.prettyPrint()} ${methods})`; } } + +export class EliminatorType extends Core { + + constructor( + public typeName: string, + public targetType: Core, + public motiveType: Core, + public methodTypes: Core[] + ) { super(); } + + public valOf(env: Environment): V.Value { + return new V.EliminatorType( + this.typeName, + this.targetType.toLazy(env), + this.motiveType.toLazy(env), + this.methodTypes.map(m => m.toLazy(env)) + ); + } + + public prettyPrint(): string { + return `EliminatorType ${this.typeName} ${this.targetType.prettyPrint()} ${this.motiveType.prettyPrint()} ${this.methodTypes.map(m => m.prettyPrint()).join(' ')}`; + } +} diff --git a/src/pie_interpreter/types/source.ts b/src/pie_interpreter/types/source.ts index 073363a3..3c9a658f 100644 --- a/src/pie_interpreter/types/source.ts +++ b/src/pie_interpreter/types/source.ts @@ -1949,14 +1949,14 @@ export class Application extends Source { } } -export class DefineDatatype extends Source { +export class InductiveDatatype extends Source { constructor( public location: Location, public typeName: string, public parameters: TypedBinder[], // Type parameters [A : Type] public indices: TypedBinder[], // Index parameters [i : Nat] public resultType: Source, // The result universe (Type) - public constructors: Constructor[] // Data constructors + public constructors: ConstructorType[] // Data constructors ) { super(location); } protected synthHelper(ctx: Context, renames: Renaming): Perhaps { @@ -1981,6 +1981,31 @@ export class DefineDatatype extends Source { } } +export class ConstructorType extends Source { + constructor( + public location: Location, + public name: string, + public args: TypedBinder[], // Constructor args + public resultType: Source // Type the constructor produces + ) { + super(location); + } + + public findNames(): string[] { + const names = [this.name]; + names.push(...this.args.flatMap(a => a.findNames())); + names.push(...this.resultType.findNames()); + return names; + } + public prettyPrint(): string { + throw new Error('Method not implemented.'); + } + protected synthHelper(ctx: Context, renames: Renaming): Perhaps { + throw new Error('Method not implemented.'); + } + +} + export class Constructor extends Source { protected synthHelper(ctx: Context, renames: Renaming): Perhaps { throw new Error('Method not implemented.'); @@ -1988,7 +2013,7 @@ export class Constructor extends Source { constructor( public location: Location, public name: string, - public args: TypedBinder[], // Constructor args + public args: Source[], // Constructor args public resultType: Source // Type the constructor produces ) { super(location); @@ -2033,4 +2058,22 @@ export class GenericEliminator extends Source { const methods = this.methods.map(m => m.prettyPrint()).join(' '); return `(elim-${this.typeName} ${this.target.prettyPrint()} ${this.motive.prettyPrint()} ${methods})`; } +} + +export class InductiveTypeInfo extends Source { + + constructor( + public location: Location, + public name: string + ) {super(location);} + public findNames(): string[] { + throw new Error('Method not implemented.'); + } + public prettyPrint(): string { + throw new Error('Method not implemented.'); + } + protected synthHelper(ctx: Context, renames: Renaming): Perhaps { + throw new Error('Method not implemented.'); + } + } \ No newline at end of file diff --git a/src/pie_interpreter/types/value.ts b/src/pie_interpreter/types/value.ts index 333f4679..aa9cbd6e 100644 --- a/src/pie_interpreter/types/value.ts +++ b/src/pie_interpreter/types/value.ts @@ -651,7 +651,7 @@ export class Constructor extends Value { constructor( public name: string, - public type: Value, + public type: string, public args: Value[], public index: number, public recursive_args: Value[], @@ -670,3 +670,43 @@ export class Constructor extends Value { return this.prettyPrint(); } } + +export class ConstructorType extends Value { + constructor( + public argTypes: Value[], + public resultType: Value + ) {super()} + public readBackType(context: Context): C.Core { + return this.resultType.readBackType(context); + } + public prettyPrint(): string { + return `ConstructorType ${this.argTypes.map(a => a.prettyPrint()).join(' ')} ${this.resultType.prettyPrint()}`; + } + +} + +export class EliminatorType extends Value { + constructor( + public typeName: string, + public targetType: Value, + public motiveType: Value, + public methodTypes: Value[] + ) { super(); } + + public readBackType(context: Context): C.Core { + return new C.EliminatorType( + this.typeName, + this.targetType.readBackType(context), + this.motiveType.readBackType(context), + this.methodTypes.map(m => m.readBackType(context)) + ); + } + + public prettyPrint(): string { + return `EliminatorType ${this.typeName} ${this.targetType.prettyPrint()} ${this.motiveType.prettyPrint()} ${this.methodTypes.map(m => m.prettyPrint()).join(' ')}`; + } + + public toString(): string { + return this.prettyPrint(); + } +} diff --git a/src/pie_interpreter/utils/context.ts b/src/pie_interpreter/utils/context.ts index 936aa6cb..ffe089c2 100644 --- a/src/pie_interpreter/utils/context.ts +++ b/src/pie_interpreter/utils/context.ts @@ -1,11 +1,11 @@ import * as C from '../types/core'; -import { Neutral, Value } from '../types/value'; +import { InductiveType, Neutral, Universe, Value, Constructor } from '../types/value'; import { Location } from './locations'; import { go, stop, Perhaps, goOn, PerhapsM, Message } from '../types/utils'; import { Environment } from './environment'; import { readBack } from '../evaluator/utils'; -import { Source } from '../types/source'; +import { Source} from '../types/source'; import { Variable } from '../types/neutral'; import { inspect } from 'util'; /* @@ -133,6 +133,14 @@ export function contextToEnvironment(ctx: Context): Environment { return env; } +export function getInductiveType(ctx: Context, where: Location, name:string): Perhaps { + for (const [n, binder] of ctx) { + if (binder instanceof InductiveDatatypeBinder && n === name) { + return new go(binder); + } + } + return new stop(where, new Message([`No inductive type found for ${name} at ${where}`])); +} export const initCtx: Context = new Map(); @@ -159,8 +167,29 @@ export class Free extends Binder { constructor(public type: Value) { super() } } +export class InductiveDatatypePlaceholder extends Binder { + type: Value = new Universe(); + constructor(public name: string) { super() } +} + +export class InductiveDatatypeBinder extends Binder { + constructor( + public name: string, + public type: InductiveType) { + super() + } +} + +export class ConstructorBinder extends Binder { + constructor( + public name: string, + public type: Constructor) { + super() + } +} + export function varType(ctx: Context, where: Location, x: string): Perhaps { - if (ctx.size === 0) { + if (ctx.size === 0) { throw new Error(`The context ${JSON.stringify(ctx)} is empty, but we are looking for ${x}`); } for (const [y, binder] of ctx.entries()) { From addd3935faaa1aceca5bf7f027d34332acf04ab9 Mon Sep 17 00:00:00 2001 From: ZhangQixiang123 Date: Wed, 3 Sep 2025 15:45:25 +0800 Subject: [PATCH 03/10] generate eliminator (hasve bugs) --- .../__tests__/test_inductive_design.ts | 237 ++++++------- .../typechecker/definedatatype.ts | 220 +++++++++--- .../typechecker/synthesizer.ts | 319 +++++++++--------- src/pie_interpreter/types/core.ts | 4 +- src/pie_interpreter/types/source.ts | 62 ++-- src/pie_interpreter/utils/context.ts | 9 + 6 files changed, 479 insertions(+), 372 deletions(-) diff --git a/src/pie_interpreter/__tests__/test_inductive_design.ts b/src/pie_interpreter/__tests__/test_inductive_design.ts index d7e5f923..993ebeae 100644 --- a/src/pie_interpreter/__tests__/test_inductive_design.ts +++ b/src/pie_interpreter/__tests__/test_inductive_design.ts @@ -1,167 +1,132 @@ import 'jest'; import * as S from '../types/source'; -import { TypedBinder, SiteBinder } from '../types/utils'; +import * as V from '../types/value'; import { Location, Syntax } from '../utils/locations'; import { Position } from '../../scheme_parser/transpiler/types/location'; +import { DefineDatatypeSource, handleDefineDatatype } from '../typechecker/definedatatype'; +import { Context } from '../utils/context'; +import { go, stop } from '../types/utils'; // Test location const testLoc = new Location(new Syntax(new Position(1, 1), new Position(1, 1), 'test'), false); -describe("Inductive Types Design Test", () => { +describe("DefineDatatype Test", () => { - it("should demonstrate ConstructorType vs Constructor distinction", () => { + it("should define a simple Bool datatype and add it to context", () => { - // ============================================ - // STEP 1: Define List datatype using ConstructorType - // ============================================ + // Create initial context + const ctx: Context = new Map(); - const listDatatype = new S.DefineDatatype( + // Define simple Bool datatype using DefineDatatypeSource + const boolDatatype = new DefineDatatypeSource( testLoc, - "List", - // Parameters: [A : Type] - [new TypedBinder(new SiteBinder(testLoc, "A"), new S.Universe(testLoc))], + "Bool", + // Parameters: (none) + [], // Indices: (none) [], - // Result type: Type - new S.Universe(testLoc), - // Constructors: ConstructorType[] (just signatures) + // Constructors with their argument types [ - // nil : List A - new S.ConstructorType( - testLoc, - "nil", - [], // no arguments - new S.Application( - testLoc, - new S.Name(testLoc, "List"), - new S.Name(testLoc, "A"), - [] - ) - ), + // true : Bool + { + name: "true", + args: [] // no arguments + }, - // cons : A -> List A -> List A - new S.ConstructorType( - testLoc, - "cons", - [ - new TypedBinder(new SiteBinder(testLoc, "head"), new S.Name(testLoc, "A")), - new TypedBinder(new SiteBinder(testLoc, "tail"), - new S.Application(testLoc, new S.Name(testLoc, "List"), new S.Name(testLoc, "A"), []) - ) - ], - new S.Application(testLoc, new S.Name(testLoc, "List"), new S.Name(testLoc, "A"), []) - ) - ] + // false : Bool + { + name: "false", + args: [] + } + ], + new V.Universe() // typeValue placeholder ); - // ============================================ - // STEP 2: Use Constructor for actual constructor calls - // ============================================ + // Handle the datatype definition - adds to context + const result = handleDefineDatatype(ctx, new Map(), boolDatatype); - // nil (no arguments) - const nilExpr = new S.Constructor( - testLoc, - "nil", - [], // no actual arguments - listDatatype - ); + // Check that the definition succeeded + expect(result).toBeInstanceOf(go); + if (result instanceof stop) { + throw new Error(`Failed to define datatype: ${result.message}`); + } - // cons 42 nil - const cons42Nil = new S.Constructor( - testLoc, - "cons", - [ - new S.Number(testLoc, 42), // head argument - nilExpr // tail argument - ], - listDatatype - ); + const updatedCtx = (result as go).result; + + // Debug: print what's in the context + console.log("Context keys:", Array.from(updatedCtx.keys())); + + // Test that datatype was added to context + expect(updatedCtx.has("Bool")).toBe(true); + + // Test that constructors were added to context + expect(updatedCtx.has("true")).toBe(true); + expect(updatedCtx.has("false")).toBe(true); + + // Test that eliminator was generated and added + expect(updatedCtx.has("elimBool")).toBe(true); + + // Test the structure of the DefineDatatypeSource + expect(boolDatatype.name).toBe("Bool"); + expect(boolDatatype.parameters).toHaveLength(0); + expect(boolDatatype.indices).toHaveLength(0); + expect(boolDatatype.constructors).toHaveLength(2); + + // Test constructor definitions + const trueCtor = boolDatatype.constructors[0]; + const falseCtor = boolDatatype.constructors[1]; - // cons 1 (cons 42 nil) - const nestedList = new S.Constructor( + expect(trueCtor.name).toBe("true"); + expect(trueCtor.args).toHaveLength(0); + + expect(falseCtor.name).toBe("false"); + expect(falseCtor.args).toHaveLength(0); + + console.log("✅ Bool datatype successfully defined and added to context!"); + }); + + it("should define a Unit datatype with single constructor", () => { + // Create initial context + const ctx: Context = new Map(); + + // Define Unit datatype (simple case with one constructor) + const unitDatatype = new DefineDatatypeSource( testLoc, - "cons", + "Unit", + [], // no parameters + [], // no indices [ - new S.Number(testLoc, 1), // head - cons42Nil // tail + // unit : Unit + { + name: "unit", + args: [] + } ], - listDatatype + new V.Universe() ); - // ============================================ - // STEP 3: Eliminator usage - // ============================================ + // Handle the datatype definition + const result = handleDefineDatatype(ctx, new Map(), unitDatatype); - const listLength = new S.GenericEliminator( - testLoc, - "List", - nestedList, // target: our nested list - // motive: List A -> Nat - new S.Lambda( - testLoc, - [new SiteBinder(testLoc, "xs")], - new S.Nat(testLoc) - ), - // methods: [nil-case, cons-case] - [ - // nil case: 0 - new S.Zero(testLoc), - - // cons case: λ head tail length_of_tail. add1 length_of_tail - new S.Lambda( - testLoc, - [ - new SiteBinder(testLoc, "head"), - new SiteBinder(testLoc, "tail"), - new SiteBinder(testLoc, "length_of_tail") - ], - new S.Add1(testLoc, new S.Name(testLoc, "length_of_tail")) - ) - ] - ); + expect(result).toBeInstanceOf(go); + if (result instanceof stop) { + throw new Error(`Failed to define Unit datatype: ${result.message}`); + } + + const updatedCtx = (result as go).result; + + // Test that all components were added to context + expect(updatedCtx.has("Unit")).toBe(true); + expect(updatedCtx.has("unit")).toBe(true); + expect(updatedCtx.has("elimUnit")).toBe(true); + + // Test structure + expect(unitDatatype.name).toBe("Unit"); + expect(unitDatatype.constructors).toHaveLength(1); + expect(unitDatatype.constructors[0].name).toBe("unit"); + expect(unitDatatype.constructors[0].args).toHaveLength(0); - // ============================================ - // STEP 4: Test the structure - // ============================================ - - // Test datatype definition structure - expect(listDatatype.typeName).toBe("List"); - expect(listDatatype.constructors).toHaveLength(2); - - // Test constructor types (in definition) - const nilCtorType = listDatatype.constructors[0]; - const consCtorType = listDatatype.constructors[1]; - - expect(nilCtorType).toBeInstanceOf(S.ConstructorType); - expect(nilCtorType.name).toBe("nil"); - expect(nilCtorType.args).toHaveLength(0); - - expect(consCtorType).toBeInstanceOf(S.ConstructorType); - expect(consCtorType.name).toBe("cons"); - expect(consCtorType.args).toHaveLength(2); - expect(consCtorType.args[0].binder.varName).toBe("head"); - expect(consCtorType.args[1].binder.varName).toBe("tail"); - - // Test constructor applications (in expressions) - expect(nilExpr).toBeInstanceOf(S.Constructor); - expect(nilExpr.name).toBe("nil"); - expect(nilExpr.args).toHaveLength(0); - - expect(cons42Nil).toBeInstanceOf(S.Constructor); - expect(cons42Nil.name).toBe("cons"); - expect(cons42Nil.args).toHaveLength(2); - expect(cons42Nil.args[0]).toBeInstanceOf(S.Number); - expect(cons42Nil.args[1]).toBeInstanceOf(S.Constructor); // nested constructor - - // Test eliminator structure - expect(listLength).toBeInstanceOf(S.GenericEliminator); - expect(listLength.typeName).toBe("List"); - expect(listLength.target).toBeInstanceOf(S.Constructor); - expect(listLength.methods).toHaveLength(2); - - console.log("✅ Design structure is correct!"); - console.log("ConstructorType used in definitions:", nilCtorType.constructor.name); - console.log("Constructor used in expressions:", nilExpr.constructor.name); + console.log("✅ Unit datatype successfully defined!"); }); // it("should demonstrate Vector with indices", () => { diff --git a/src/pie_interpreter/typechecker/definedatatype.ts b/src/pie_interpreter/typechecker/definedatatype.ts index 4e68b96e..0f3c3821 100644 --- a/src/pie_interpreter/typechecker/definedatatype.ts +++ b/src/pie_interpreter/typechecker/definedatatype.ts @@ -1,8 +1,8 @@ import * as S from '../types/source'; import * as C from '../types/core'; import * as V from '../types/value'; -import { go, goOn, Perhaps, stop } from '../types/utils'; -import { Context, extendContext, getInductiveType, InductiveDatatypePlaceholder, InductiveDatatypeBinder, ConstructorBinder, contextToEnvironment } from '../utils/context'; +import { go, goOn, Perhaps, stop, fresh, TypedBinder, Message } from '../types/utils'; +import { Context, extendContext, getInductiveType, InductiveDatatypePlaceholder, InductiveDatatypeBinder, ConstructorBinder, contextToEnvironment, EliminatorBinder, valInContext } from '../utils/context'; import { Location } from '../utils/locations'; import { rename, Renaming } from './utils'; import { Constructor } from '../types/value'; @@ -32,55 +32,38 @@ export class DefineDatatypeSource { }) const synthedIndices = this.indices.map(p => p.type.isType(ctx, rename)) .map(p => { - if (p instanceof stop) { - throw new Error(`Index type is not a type at ${p.where}`) - } - return (p as go).result - }) - let counter = 0 + if (p instanceof stop) { + throw new Error(`Index type is not a type at ${p.where}`) + } + return (p as go).result + }) + + let counter = 0; const synthedConstructors = this.constructors.map( p => { - let rec_args: S.InductiveTypeInfo[] = [] - counter += 1 - const typecheckedArgs = p.args.map( - arg => { - if (arg.type instanceof S.InductiveTypeInfo) { - if (arg.type.name === this.name) { - rec_args = [...rec_args, arg.type] - return arg.type.isType(ctx, rename) - } -//TODO: Probably this else is negligible, becuase we need to add check inductive type in isType - else { - const inductiveTypeTemp = getInductiveType(ctx, arg.location, arg.type.name) - if (inductiveTypeTemp instanceof stop) { - throw new Error(`No inductive type found for ${arg.type.name} at ${arg.location}`) - } - return new go((inductiveTypeTemp as go).result.type.readBackType(ctx)) - } - } else { - return arg.type.isType(ctx, rename) - } - } - ).map(p => { - if (p instanceof stop) { - throw new Error(`Constructor argument type is not a type at ${p.where}`) - } - return (p as go).result - }) - const coreRecArgs = rec_args.map(recArg => recArg.isType(ctx, rename)) - .map(p => { - if (p instanceof stop) { - throw new Error(`Recursive argument type is not a type at ${p.where}`) + const typecheckedArgs = p.args.map(arg => arg.isType(ctx, rename)) + .map(arg => { + if (arg instanceof stop) { + throw new Error(`Constructor argument type is not a type at ${arg.where}`) + } + return (arg as go).result + }) + + // Find recursive arguments (those with type T) + const coreRecArgs = p.args.filter(arg => + arg.prettyPrint().includes(this.name) + ).map(arg => arg.isType(ctx, rename)) + .map(arg => { + if (arg instanceof stop) { + throw new Error(`Recursive argument type is not a type at ${arg.where}`) } - return (p as go).result + return (arg as go).result }) - return new C.Constructor(p.name, this.name, typecheckedArgs, counter, coreRecArgs) + return new C.Constructor(p.name, this.name, typecheckedArgs, counter++, coreRecArgs) } ) return new go(new DefineDatatypeCore(this.name, synthedParameters, synthedIndices, synthedConstructors)) } - - } export class DefineDatatypeCore { @@ -96,7 +79,85 @@ export class DefineDatatypeCore { this.name, this.parameters.map(p => p.toLazy(env)), this.indices.map(i => i.toLazy(env)), -) } + ) + } +} + +// Eliminator binder to store eliminator type information in context +export class EliminatorGenerator { + constructor( + public name: string, + public datatypeName: string, + public parameters: C.Core[], + public indices: C.Core[], + public constructors: C.Constructor[] + ) {} + + public generateEliminatorType(ctx: Context): C.Core { + // Following the algorithm: (Π [v : T A ... iv...] [P : (Π [i : τi]... (→ (T A ... i ...) Type))] [m ...]... (P iv... v)) + + // 1. Target type: (T A ... iv...) + let targetType: C.Core = new C.VarName(this.datatypeName); + for (const param of this.parameters) { + targetType = new C.Application(targetType, param); + } + for (const index of this.indices) { + targetType = new C.Application(targetType, index); + } + + // 2. Motive type: (Π [i : τi]... (→ (T A ... i ...) Type)) + let motiveType: C.Core = new C.Pi( + fresh(ctx, "target"), + targetType, + new C.Universe() + ); + + // 3. Method types: one for each constructor + const methodTypes = this.constructors.map(ctor => this.generateMethodType(ctx, ctor, motiveType)); + + // 4. Build the full eliminator type + let elimType: C.Core = motiveType; // Start with motive result type + + // Add methods from right to left + for (let i = methodTypes.length - 1; i >= 0; i--) { + elimType = new C.Pi(fresh(ctx, `method_${i}`), methodTypes[i], elimType); + } + + // Add motive + elimType = new C.Pi(fresh(ctx, "motive"), motiveType, elimType); + + // Add target + elimType = new C.Pi(fresh(ctx, "target"), targetType, elimType); + + return elimType; + } + + private generateMethodType(ctx: Context, ctor: C.Constructor, motiveType: C.Core): C.Core { + // Following algorithm: (Π [i+x : τ1]... (→ (P ix... xrec)... (P τ2i... (C A... i+x...)))) + + // Build constructor application: (C A... i+x...) + let ctorApp: C.Core = new C.VarName(ctor.name); + + // Apply parameters and constructor args + for (const param of this.parameters) { + ctorApp = new C.Application(ctorApp, param); + } + + let resultType: C.Core = new C.Application(motiveType, ctorApp); + + // Add inductive hypotheses for recursive arguments + for (const recArg of ctor.recursive_args) { + const ihType = new C.Application(motiveType, recArg); + resultType = new C.Pi(fresh(ctx, "ih"), ihType, resultType); + } + + // Add constructor arguments + for (let i = ctor.args.length - 1; i >= 0; i--) { + resultType = new C.Pi(fresh(ctx, `arg_${i}`), ctor.args[i], resultType); + } + + return resultType; + } } export function handleDefineDatatype(ctx: Context, renaming: Renaming, target: DefineDatatypeSource): Perhaps { @@ -114,11 +175,82 @@ export function handleDefineDatatype(ctx: Context, renaming: Renaming, target: D const core = (synthesized as go).result ctx.delete(target.name) + // 1. Add the datatype itself extendContext(ctx, core.name, new InductiveDatatypeBinder(core.name, core.valOf(contextToEnvironment(ctx)))) + // 2. Add each constructor for (const ctor of core.constructors) { extendContext(ctx, ctor.name, new ConstructorBinder(ctor.name, ctor.valOf(contextToEnvironment(ctx)))) } + // 3. Generate and add the eliminator (following the algorithm) + const eliminatorName = `elim${core.name}`; + const eliminatorGenerator = new EliminatorGenerator( + eliminatorName, + core.name, + core.parameters, + core.indices, + core.constructors + ); + + // Add eliminator to context + extendContext(ctx, eliminatorName, new EliminatorBinder(eliminatorName, valInContext(ctx, eliminatorGenerator.generateEliminatorType(ctx)))); + return new go(ctx) +} + +// Type synthesis for eliminator applications +export function synthEliminator( + ctx: Context, + renaming: Renaming, + location: Location, + elimName: string, + target: S.Source, + motive: S.Source, + methods: S.Source[] +): Perhaps { + + // Get eliminator from context + const elimBinder = ctx.get(elimName); + if (!elimBinder || !(elimBinder instanceof EliminatorGenerator)) { + return new stop(location, new Message([`Unknown eliminator: ${elimName}`])); + } + + // 1. Check target type: must be (T A ... iv...) + const targetSynth = target.synth(ctx, renaming); + if (targetSynth instanceof stop) return targetSynth; + + // 2. Check motive type: must be (Π [i : τi]... (→ (T A ... i ...) Type)) + const motiveSynth = motive.synth(ctx, renaming); + if (motiveSynth instanceof stop) return motiveSynth; + + // 3. Check each method type against corresponding constructor + if (methods.length !== elimBinder.constructors.length) { + return new stop(location, new Message([ + `Eliminator expects ${elimBinder.constructors.length} methods, got ${methods.length}` + ])); + } + + for (let i = 0; i < methods.length; i++) { + const methodSynth = methods[i].synth(ctx, renaming); + if (methodSynth instanceof stop) return methodSynth; + + // TODO: Check method type matches expected type for constructor i + } + + // Result type: (P iv... v) - motive applied to target + const resultType = new C.Application( + (motiveSynth as go).result.type, + (targetSynth as go).result.expr + ); + + return new go(new C.The( + resultType, + new C.Eliminator( + elimBinder.datatypeName, + (targetSynth as go).result.expr, + (motiveSynth as go).result.expr, + methods.map((m, i) => ((m.synth(ctx, renaming) as go).result.expr)) + ) + )); } \ No newline at end of file diff --git a/src/pie_interpreter/typechecker/synthesizer.ts b/src/pie_interpreter/typechecker/synthesizer.ts index e065e17b..7a8b9923 100644 --- a/src/pie_interpreter/typechecker/synthesizer.ts +++ b/src/pie_interpreter/typechecker/synthesizer.ts @@ -13,7 +13,7 @@ import { notForInfo } from "../utils/locations"; import { doApp, doCar, indVecStepType } from "../evaluator/evaluator"; import { readBack } from '../evaluator/utils'; import { Location } from '../utils/locations'; -import { ConstructorType, DefineDatatype } from '../types/source'; +import { ConstructorType} from '../types/source'; import { alphaEquiv } from "../utils/alphaeqv"; @@ -1492,181 +1492,182 @@ export class synthesizer { } } - public static synthDataType(context: Context, r: Renaming, datatype: S.DefineDatatype): Perhaps { + +// public static synthDataType(context: Context, r: Renaming, datatype: S.DefineDatatype): Perhaps { - } +// } - public static GenerateConstructor( - ctx: Context, - renames: Renaming, - datatype: S.DefineDatatype - ): Perhaps { +// public static GenerateConstructor( +// ctx: Context, +// renames: Renaming, +// datatype: S.DefineDatatype +// ): Perhaps { - let buildConstructorApplication = (constructorName: string, argNames: string[], datatypeName: string, parameters: C.Core[], indices: C.Core[]): C.Core => { - let result: C.Core = new C.VarName(datatypeName); +// let buildConstructorApplication = (constructorName: string, argNames: string[], datatypeName: string, parameters: C.Core[], indices: C.Core[]): C.Core => { +// let result: C.Core = new C.VarName(datatypeName); - // Apply parameters - for (const param of parameters) { - result = new C.Application(result, param); - } +// // Apply parameters +// for (const param of parameters) { +// result = new C.Application(result, param); +// } - // Apply indices - for (const index of indices) { - result = new C.Application(result, index); - } +// // Apply indices +// for (const index of indices) { +// result = new C.Application(result, index); +// } - // Apply constructor - let constructorApp: C.Core = new C.VarName(constructorName); - for (const argName of argNames) { - constructorApp = new C.Application(constructorApp, new C.VarName(argName)); - } +// // Apply constructor +// let constructorApp: C.Core = new C.VarName(constructorName); +// for (const argName of argNames) { +// constructorApp = new C.Application(constructorApp, new C.VarName(argName)); +// } - return constructorApp; - }; - - let generateMethodType = ( - constructorName: string, - argTypes: C.Core[], - rec_args: C.Core[], - resultType: C.Core, - motive: C.Core, - datatypeName: string, - parameters: C.Core[], - indices: C.Core[] - ): C.Core => { - let argNames: string[] = []; - let recArgNames: string[] = []; +// return constructorApp; +// }; + +// let generateMethodType = ( +// constructorName: string, +// argTypes: C.Core[], +// rec_args: C.Core[], +// resultType: C.Core, +// motive: C.Core, +// datatypeName: string, +// parameters: C.Core[], +// indices: C.Core[] +// ): C.Core => { +// let argNames: string[] = []; +// let recArgNames: string[] = []; - // Generate argument names - for (let i = 0; i < argTypes.length; i++) { - argNames.push(fresh(ctx, `arg_${i}`)); - } +// // Generate argument names +// for (let i = 0; i < argTypes.length; i++) { +// argNames.push(fresh(ctx, `arg_${i}`)); +// } - // Generate inductive hypothesis names - for (let i = 0; i < rec_args.length; i++) { - recArgNames.push(fresh(ctx, `ih_${i}`)); - } +// // Generate inductive hypothesis names +// for (let i = 0; i < rec_args.length; i++) { +// recArgNames.push(fresh(ctx, `ih_${i}`)); +// } - // Build the constructor application - const constructorApp = buildConstructorApplication(constructorName, argNames, datatypeName, parameters, indices); +// // Build the constructor application +// const constructorApp = buildConstructorApplication(constructorName, argNames, datatypeName, parameters, indices); - // Final result type: motive applied to constructor application - let methodType: C.Core = new C.Application(motive, constructorApp); +// // Final result type: motive applied to constructor application +// let methodType: C.Core = new C.Application(motive, constructorApp); - // Add inductive hypotheses (right to left) - for (let i = rec_args.length - 1; i >= 0; i--) { - const ihName = recArgNames[i]; - const recArgApp = new C.Application(motive, new C.VarName(argNames[i])); // Apply motive to recursive argument +// // Add inductive hypotheses (right to left) +// for (let i = rec_args.length - 1; i >= 0; i--) { +// const ihName = recArgNames[i]; +// const recArgApp = new C.Application(motive, new C.VarName(argNames[i])); // Apply motive to recursive argument - methodType = new C.Pi( - ihName, - recArgApp, - methodType - ); - } +// methodType = new C.Pi( +// ihName, +// recArgApp, +// methodType +// ); +// } - // Add constructor arguments (right to left) - for (let i = argTypes.length - 1; i >= 0; i--) { - const argName = argNames[i]; - methodType = new C.Pi( - argName, - argTypes[i], - methodType - ); - } +// // Add constructor arguments (right to left) +// for (let i = argTypes.length - 1; i >= 0; i--) { +// const argName = argNames[i]; +// methodType = new C.Pi( +// argName, +// argTypes[i], +// methodType +// ); +// } - return methodType; - }; - const resultType = new PerhapsM('resultType'); - const parameters = new PerhapsM('parameters'); - const indices = new PerhapsM('indices'); - const constructorTypes = new PerhapsM('constructorTypes'); - const eliminatorTypes = new PerhapsM('eliminatorTypes'); - - return goOn( - [ - [resultType, () => datatype.resultType.check(ctx, renames, new V.Universe())], - [parameters, () => datatype.parameters.map((param) => param.type.check(ctx, renames, new V.Universe()))], - [indices, () => datatype.indices.map((index) => index.type.check(ctx, renames, new V.Universe()))], - [constructorTypes, () => datatype.constructors.map((constructor) => this.checkConstructorType(ctx, renames, constructor as S.ConstructorType))], - [eliminatorTypes, () => { - const resultTypeResult = resultType.value; - const parametersResults = parameters.value; - const indicesResults = indices.value; - const constructorTypesResults = constructorTypes.value; - const motiveType = new C.Pi( - 'test_input_fst', - resultTypeResult, - new C.Universe() - ) +// return methodType; +// }; +// const resultType = new PerhapsM('resultType'); +// const parameters = new PerhapsM('parameters'); +// const indices = new PerhapsM('indices'); +// const constructorTypes = new PerhapsM('constructorTypes'); +// const eliminatorTypes = new PerhapsM('eliminatorTypes'); + +// return goOn( +// [ +// [resultType, () => datatype.resultType.check(ctx, renames, new V.Universe())], +// [parameters, () => datatype.parameters.map((param) => param.type.check(ctx, renames, new V.Universe()))], +// [indices, () => datatype.indices.map((index) => index.type.check(ctx, renames, new V.Universe()))], +// [constructorTypes, () => datatype.constructors.map((constructor) => this.checkConstructorType(ctx, renames, constructor as S.ConstructorType))], +// [eliminatorTypes, () => { +// const resultTypeResult = resultType.value; +// const parametersResults = parameters.value; +// const indicesResults = indices.value; +// const constructorTypesResults = constructorTypes.value; +// const motiveType = new C.Pi( +// 'test_input_fst', +// resultTypeResult, +// new C.Universe() +// ) - }] - ], - () => new go( - new C.The( - new C.Universe(), - new C.InductiveType( - datatype.typeName, - parameters.value, - indices.value - ) - ) - ) - ); - - } - - public static checkConstructorType(ctx: Context, renames: Renaming, ConstructorType: S.ConstructorType): Perhaps { - const normalizedResultTypeTemp = ConstructorType.resultType.check(ctx, renames, new V.Universe()); - - let binder = ConstructorType.args; - - let normalizedType = [] - for (const param of binder) { - const paramCheck = param.type.check(ctx, renames, new V.Universe()); - if (paramCheck instanceof stop) return paramCheck; - normalizedType.push((paramCheck as go).result); - } - - let recur_args = [] - let normalizedResultType = (normalizedResultTypeTemp as go).result - - for (const arg of normalizedType) { - if (alphaEquiv(arg, normalizedResultType)) { - recur_args.push(arg); - } - } - - return new go(new C.ConstructorType( - normalizedType, - recur_args, - (normalizedResultTypeTemp as go).result - )); - } -} - -function checkAndBuildTypes(ctx: Context, renames: Renaming, initialType: C.Core, binder: TypedBinder[]): Perhaps { - let normalizedType = [] - for (const param of binder) { - const paramCheck = param.type.check(ctx, renames, new V.Universe()); - if (paramCheck instanceof stop) return paramCheck; - normalizedType.push((paramCheck as go).result); - } - - let cur_Type = initialType - for (let i = normalizedType.length - 1; i >= 0; i--) { - const paramType = normalizedType[i]; - const paramName = binder[i].findNames(); - const currentTType = cur_Type; - cur_Type = new V.Pi( - paramName, - valInContext(ctx, paramType), - new HigherOrderClosure((v: V.Value) => currentTType) - ); - } - - return new go(cur_Type); +// }] +// ], +// () => new go( +// new C.The( +// new C.Universe(), +// new C.InductiveType( +// datatype.typeName, +// parameters.value, +// indices.value +// ) +// ) +// ) +// ); + +// } + +// public static checkConstructorType(ctx: Context, renames: Renaming, ConstructorType: S.ConstructorType): Perhaps { +// const normalizedResultTypeTemp = ConstructorType.resultType.check(ctx, renames, new V.Universe()); + +// let binder = ConstructorType.args; + +// let normalizedType = [] +// for (const param of binder) { +// const paramCheck = param.type.check(ctx, renames, new V.Universe()); +// if (paramCheck instanceof stop) return paramCheck; +// normalizedType.push((paramCheck as go).result); +// } + +// let recur_args = [] +// let normalizedResultType = (normalizedResultTypeTemp as go).result + +// for (const arg of normalizedType) { +// if (alphaEquiv(arg, normalizedResultType)) { +// recur_args.push(arg); +// } +// } + +// return new go(new C.ConstructorType( +// normalizedType, +// recur_args, +// (normalizedResultTypeTemp as go).result +// )); +// } +// } + +// function checkAndBuildTypes(ctx: Context, renames: Renaming, initialType: C.Core, binder: TypedBinder[]): Perhaps { +// let normalizedType = [] +// for (const param of binder) { +// const paramCheck = param.type.check(ctx, renames, new V.Universe()); +// if (paramCheck instanceof stop) return paramCheck; +// normalizedType.push((paramCheck as go).result); +// } + +// let cur_Type = initialType +// for (let i = normalizedType.length - 1; i >= 0; i--) { +// const paramType = normalizedType[i]; +// const paramName = binder[i].findNames(); +// const currentTType = cur_Type; +// cur_Type = new V.Pi( +// paramName, +// valInContext(ctx, paramType), +// new HigherOrderClosure((v: V.Value) => currentTType) +// ); +// } + +// return new go(cur_Type); } \ No newline at end of file diff --git a/src/pie_interpreter/types/core.ts b/src/pie_interpreter/types/core.ts index f38c7436..fa0ed370 100644 --- a/src/pie_interpreter/types/core.ts +++ b/src/pie_interpreter/types/core.ts @@ -1094,8 +1094,8 @@ export class InductiveType extends Core { public typeName: string, public parameters: Core[], public indices: Core[], - public constructorTypes: Core[], - public eliminatorType: Core[] + // public constructorTypes: Core[], + // public eliminatorType: Core[] ) { super(); } public prettyPrint(): string { diff --git a/src/pie_interpreter/types/source.ts b/src/pie_interpreter/types/source.ts index 3c9a658f..dcc87b1c 100644 --- a/src/pie_interpreter/types/source.ts +++ b/src/pie_interpreter/types/source.ts @@ -1949,37 +1949,37 @@ export class Application extends Source { } } -export class InductiveDatatype extends Source { - constructor( - public location: Location, - public typeName: string, - public parameters: TypedBinder[], // Type parameters [A : Type] - public indices: TypedBinder[], // Index parameters [i : Nat] - public resultType: Source, // The result universe (Type) - public constructors: ConstructorType[] // Data constructors - ) { super(location); } - - protected synthHelper(ctx: Context, renames: Renaming): Perhaps { - return Synth.synthDefineDatatype(ctx, renames, this); - } - - public findNames(): string[] { - const names = [this.typeName]; - names.push(...this.parameters.flatMap(p => p.findNames())); - names.push(...this.indices.flatMap(i => i.findNames())); - names.push(...this.resultType.findNames()); - names.push(...this.constructors.flatMap(c => c.findNames())); - return names; - } - - public prettyPrint(): string { - const params = this.parameters.map(p => `[${p.prettyPrint()}]`).join(' '); - const indices = this.indices.map(i => `[${i.prettyPrint()}]`).join(' '); - const ctors = this.constructors.map(c => c.prettyPrint()).join('\n '); - return `(define-datatype ${this.typeName} ${params} : ${indices} ${this.resultType.prettyPrint()} - ${ctors})`; - } -} +// export class InductiveDatatype extends Source { +// constructor( +// public location: Location, +// public typeName: string, +// public parameters: TypedBinder[], // Type parameters [A : Type] +// public indices: TypedBinder[], // Index parameters [i : Nat] +// public resultType: Source, // The result universe (Type) +// public constructors: ConstructorType[] // Data constructors +// ) { super(location); } + +// protected synthHelper(ctx: Context, renames: Renaming): Perhaps { +// return Synth.synthDefineDatatype(ctx, renames, this); +// } + +// public findNames(): string[] { +// const names = [this.typeName]; +// names.push(...this.parameters.flatMap(p => p.findNames())); +// names.push(...this.indices.flatMap(i => i.findNames())); +// names.push(...this.resultType.findNames()); +// names.push(...this.constructors.flatMap(c => c.findNames())); +// return names; +// } + +// public prettyPrint(): string { +// const params = this.parameters.map(p => `[${p.prettyPrint()}]`).join(' '); +// const indices = this.indices.map(i => `[${i.prettyPrint()}]`).join(' '); +// const ctors = this.constructors.map(c => c.prettyPrint()).join('\n '); +// return `(define-datatype ${this.typeName} ${params} : ${indices} ${this.resultType.prettyPrint()} +// ${ctors})`; +// } +// } export class ConstructorType extends Source { constructor( diff --git a/src/pie_interpreter/utils/context.ts b/src/pie_interpreter/utils/context.ts index ffe089c2..7f342e42 100644 --- a/src/pie_interpreter/utils/context.ts +++ b/src/pie_interpreter/utils/context.ts @@ -8,6 +8,7 @@ import { readBack } from '../evaluator/utils'; import { Source} from '../types/source'; import { Variable } from '../types/neutral'; import { inspect } from 'util'; +import { Eliminator } from '../types/core'; /* ## Contexts ## A context maps free variable names to binders. @@ -188,6 +189,14 @@ export class ConstructorBinder extends Binder { } } +export class EliminatorBinder extends Binder { + constructor( + public name: string, + public type: Value) { + super() + } +} + export function varType(ctx: Context, where: Location, x: string): Perhaps { if (ctx.size === 0) { throw new Error(`The context ${JSON.stringify(ctx)} is empty, but we are looking for ${x}`); From 30be76d31bb3d46644f02561e2d2672237ff74e7 Mon Sep 17 00:00:00 2001 From: ZhangQixiang123 Date: Thu, 18 Sep 2025 23:09:05 +0800 Subject: [PATCH 04/10] in prograss --- .../__tests__/test_inductive_design.ts | 480 ++++++++++++++---- .../__tests__/test_integration.ts | 161 ++++++ .../__tests__/test_telescope.ts | 10 + src/pie_interpreter/evaluator/evaluator.ts | 4 +- .../typechecker/definedatatype.ts | 274 +++++++--- src/pie_interpreter/types/source.ts | 161 +++++- src/pie_interpreter/utils/context.ts | 2 + 7 files changed, 912 insertions(+), 180 deletions(-) create mode 100644 src/pie_interpreter/__tests__/test_integration.ts create mode 100644 src/pie_interpreter/__tests__/test_telescope.ts diff --git a/src/pie_interpreter/__tests__/test_inductive_design.ts b/src/pie_interpreter/__tests__/test_inductive_design.ts index 993ebeae..6f6c63b2 100644 --- a/src/pie_interpreter/__tests__/test_inductive_design.ts +++ b/src/pie_interpreter/__tests__/test_inductive_design.ts @@ -1,11 +1,16 @@ import 'jest'; import * as S from '../types/source'; import * as V from '../types/value'; +import * as C from '../types/core'; +import * as N from '../types/neutral'; +import * as Evaluator from '../evaluator/evaluator'; import { Location, Syntax } from '../utils/locations'; import { Position } from '../../scheme_parser/transpiler/types/location'; -import { DefineDatatypeSource, handleDefineDatatype } from '../typechecker/definedatatype'; -import { Context } from '../utils/context'; -import { go, stop } from '../types/utils'; +import { DefineDatatypeSource, handleDefineDatatype, makeTypedBinder, makeConstructorSpec } from '../typechecker/definedatatype'; +import { Context, contextToEnvironment } from '../utils/context'; +import { go, stop, HigherOrderClosure, TypedBinder } from '../types/utils'; +import { Environment } from '../utils/environment'; +import { readBack } from '../evaluator/utils'; // Test location const testLoc = new Location(new Syntax(new Position(1, 1), new Position(1, 1), 'test'), false); @@ -24,22 +29,15 @@ describe("DefineDatatype Test", () => { // Parameters: (none) [], // Indices: (none) - [], + [], // Constructors with their argument types [ // true : Bool - { - name: "true", - args: [] // no arguments - }, - + makeConstructorSpec("true", []), // no arguments + // false : Bool - { - name: "false", - args: [] - } - ], - new V.Universe() // typeValue placeholder + makeConstructorSpec("false", []) + ] ); // Handle the datatype definition - adds to context @@ -54,7 +52,7 @@ describe("DefineDatatype Test", () => { const updatedCtx = (result as go).result; // Debug: print what's in the context - console.log("Context keys:", Array.from(updatedCtx.keys())); + console.log("Context keys:", updatedCtx); // Test that datatype was added to context expect(updatedCtx.has("Bool")).toBe(true); @@ -64,7 +62,7 @@ describe("DefineDatatype Test", () => { expect(updatedCtx.has("false")).toBe(true); // Test that eliminator was generated and added - expect(updatedCtx.has("elimBool")).toBe(true); + expect(updatedCtx.has("elim-Bool")).toBe(true); // Test the structure of the DefineDatatypeSource expect(boolDatatype.name).toBe("Bool"); @@ -97,12 +95,8 @@ describe("DefineDatatype Test", () => { [], // no indices [ // unit : Unit - { - name: "unit", - args: [] - } - ], - new V.Universe() + makeConstructorSpec("unit", []) + ] ); // Handle the datatype definition @@ -118,7 +112,7 @@ describe("DefineDatatype Test", () => { // Test that all components were added to context expect(updatedCtx.has("Unit")).toBe(true); expect(updatedCtx.has("unit")).toBe(true); - expect(updatedCtx.has("elimUnit")).toBe(true); + expect(updatedCtx.has("elim-Unit")).toBe(true); // Test structure expect(unitDatatype.name).toBe("Unit"); @@ -128,83 +122,365 @@ describe("DefineDatatype Test", () => { console.log("✅ Unit datatype successfully defined!"); }); + + it("should integrate high-level datatype definition with proper Source constructors", () => { + // Create initial context + const ctx: Context = new Map(); + + // Define Bool datatype using high-level system + const boolDatatype = new DefineDatatypeSource( + testLoc, + "Bool", + [], // no parameters + [], // no indices + [ + makeConstructorSpec("true", []), + makeConstructorSpec("false", []) + ] + ); + + // Handle the datatype definition - adds to context + const result = handleDefineDatatype(ctx, new Map(), boolDatatype); + expect(result).toBeInstanceOf(go); + if (result instanceof stop) { + throw new Error(`Failed to define Bool datatype: ${result.message}`); + } + + const updatedCtx = (result as go).result; + + // Verify components were added to context + expect(updatedCtx.has("Bool")).toBe(true); + expect(updatedCtx.has("true")).toBe(true); + expect(updatedCtx.has("false")).toBe(true); + expect(updatedCtx.has("elim-Bool")).toBe(true); + + // Now use proper Source constructors that reference the context + + // Create constructor applications using Source constructors + const trueSource = new S.ConstructorApplication(testLoc, "true", []); + const falseSource = new S.ConstructorApplication(testLoc, "false", []); + + // Synthesize the constructor applications through proper pipeline + const trueSynth = trueSource.synth(updatedCtx, new Map()); + const falseSynth = falseSource.synth(updatedCtx, new Map()); + + expect(trueSynth).toBeInstanceOf(go); + expect(falseSynth).toBeInstanceOf(go); + + if (trueSynth instanceof go && falseSynth instanceof go) { + // Verify that the Source constructors work properly through synthesis + + // Test that we can get the Core expressions + const trueCore = trueSynth.result.expr; + const falseCore = falseSynth.result.expr; + + // The expression should be a Constructor + expect(trueCore).toBeInstanceOf(C.Constructor); + expect(falseCore).toBeInstanceOf(C.Constructor); + + if (trueCore instanceof C.Constructor && falseCore instanceof C.Constructor) { + expect(trueCore.name).toBe("true"); + expect(falseCore.name).toBe("false"); + expect(trueCore.index).toBe(0); + expect(falseCore.index).toBe(1); + } + } + + console.log("✅ Bool datatype with proper Source constructors successfully executed!"); + }); + + it("should demonstrate proper Source constructor lookup from context", () => { + // Create initial context and define Bool datatype + const ctx: Context = new Map(); + const boolDatatype = new DefineDatatypeSource( + testLoc, + "Bool", + [], [], + [makeConstructorSpec("true", []), makeConstructorSpec("false", [])] + ); + + const result = handleDefineDatatype(ctx, new Map(), boolDatatype); + expect(result).toBeInstanceOf(go); + const updatedCtx = (result as go).result; + + // Test that our new ConstructorApplication can find constructors in context + const trueSource = new S.ConstructorApplication(testLoc, "true", []); + const falseSource = new S.ConstructorApplication(testLoc, "false", []); + + // Test that synthesis works (finds constructors in context) + const trueSynth = trueSource.synth(updatedCtx, new Map()); + const falseSynth = falseSource.synth(updatedCtx, new Map()); + + expect(trueSynth).toBeInstanceOf(go); + expect(falseSynth).toBeInstanceOf(go); + + // Test that unknown constructor fails properly + const unknownSource = new S.ConstructorApplication(testLoc, "unknown", []); + + expect(() => { + unknownSource.synth(updatedCtx, new Map()); + }).toThrow("Unknown constructor: unknown"); + + console.log("✅ Source constructors properly lookup from context!"); + }); + + it("should demonstrate proper Source eliminator lookup from context", () => { + // Create initial context and define Bool datatype + const ctx: Context = new Map(); + const boolDatatype = new DefineDatatypeSource( + testLoc, + "Bool", + [], [], + [makeConstructorSpec("true", []), makeConstructorSpec("false", [])] + ); + + const result = handleDefineDatatype(ctx, new Map(), boolDatatype); + expect(result).toBeInstanceOf(go); + const updatedCtx = (result as go).result; + + // Test that our new EliminatorApplication can find eliminators in context + const trueSource = new S.ConstructorApplication(testLoc, "true", []); + + // Create simple methods (we'll use Name references to existing values in context) + const method1 = new S.Zero(testLoc); + const method2 = new S.Zero(testLoc); + + // Create eliminator application using Source + const eliminatorSource = new S.EliminatorApplication( + testLoc, + "Bool", + trueSource, + new S.Nat(testLoc), // simplified motive + [method1, method2] + ); + + // Test that eliminator synthesis works (finds inductive type and eliminator in context) + const eliminatorSynth = eliminatorSource.synth(updatedCtx, new Map()); + expect(eliminatorSynth).toBeInstanceOf(go); + + // Test that unknown eliminator fails properly + const unknownEliminatorSource = new S.EliminatorApplication( + testLoc, + "UnknownType", + trueSource, + new S.Nat(testLoc), + [method1] + ); + + expect(() => { + unknownEliminatorSource.synth(updatedCtx, new Map()); + }).toThrow(); // Should fail due to unknown type not in context + + console.log("✅ Source eliminators properly lookup from context!"); + }); + + it("should create and eliminate a Nat-like datatype", () => { + // Create initial context + const ctx: Context = new Map(); + + // Define MyNat datatype (similar to natural numbers) - simplified without self-reference for now + const myNatDatatype = new DefineDatatypeSource( + testLoc, + "MyNat", + [], // no parameters + [], // no indices + [ + makeConstructorSpec("myZero", []), + makeConstructorSpec("myAdd1", []) // Simplified to avoid self-reference parsing issues + ] + ); + + // Handle the datatype definition + const result = handleDefineDatatype(ctx, new Map(), myNatDatatype); + expect(result).toBeInstanceOf(go); + if (result instanceof stop) { + throw new Error(`Failed to define MyNat datatype: ${result.message}`); + } + + const updatedCtx = (result as go).result; + + // Verify components were added to context + expect(updatedCtx.has("MyNat")).toBe(true); + expect(updatedCtx.has("myZero")).toBe(true); + expect(updatedCtx.has("myAdd1")).toBe(true); + expect(updatedCtx.has("elim-MyNat")).toBe(true); + + // Use proper Source constructors instead of creating Values directly + const myZeroSource = new S.ConstructorApplication(testLoc, "myZero", []); + const myAdd1Source = new S.ConstructorApplication(testLoc, "myAdd1", []); + + // Test type-checking through proper Source synthesis + const myZeroSynth = myZeroSource.synth(updatedCtx, new Map()); + const myAdd1Synth = myAdd1Source.synth(updatedCtx, new Map()); + + expect(myZeroSynth).toBeInstanceOf(go); + expect(myAdd1Synth).toBeInstanceOf(go); + + if (myZeroSynth instanceof go && myAdd1Synth instanceof go) { + // Verify the synthesized Core expressions + const myZeroCore = myZeroSynth.result.expr; + const myAdd1Core = myAdd1Synth.result.expr; + + expect(myZeroCore).toBeInstanceOf(C.Constructor); + expect(myAdd1Core).toBeInstanceOf(C.Constructor); + + if (myZeroCore instanceof C.Constructor && myAdd1Core instanceof C.Constructor) { + // Test that constructors have correct names and indices + expect(myZeroCore.name).toBe("myZero"); + expect(myAdd1Core.name).toBe("myAdd1"); + expect(myZeroCore.type).toBe("MyNat"); + expect(myAdd1Core.type).toBe("MyNat"); + expect(myZeroCore.index).toBe(0); + expect(myAdd1Core.index).toBe(1); + + // Test that we can create an eliminator using Source constructors + const motiveSource = new S.Nat(testLoc); // Simple motive: MyNat -> Nat + const method1Source = new S.Zero(testLoc); // myZero -> 0 + const method2Source = new S.Add1(testLoc, new S.Zero(testLoc)); // myAdd1 -> 1 + + const eliminatorSource = new S.EliminatorApplication( + testLoc, + "MyNat", + myZeroSource, // target + motiveSource, // motive + [method1Source, method2Source] // methods + ); + + // Test that eliminator synthesis works through type-checking + const eliminatorSynth = eliminatorSource.synth(updatedCtx, new Map()); + expect(eliminatorSynth).toBeInstanceOf(go); + + // NOW ADD EVALUATION TESTS - actually evaluate the constructed sources + const myZeroValue = myZeroSynth.result.expr.valOf(contextToEnvironment(updatedCtx)); + const myAdd1Value = myAdd1Synth.result.expr.valOf(contextToEnvironment(updatedCtx)); + + // Verify the evaluated values are proper constructors + expect(myZeroValue).toBeInstanceOf(V.Constructor); + expect(myAdd1Value).toBeInstanceOf(V.Constructor); + + if (myZeroValue instanceof V.Constructor && myAdd1Value instanceof V.Constructor) { + expect(myZeroValue.name).toBe("myZero"); + expect(myAdd1Value.name).toBe("myAdd1"); + console.log("✅ Evaluation: myZero =", myZeroValue.name, "myAdd1 =", myAdd1Value.name); + } + + // Test eliminator evaluation + if (eliminatorSynth instanceof go) { + const eliminatorValue = eliminatorSynth.result.expr.valOf(contextToEnvironment(updatedCtx)); + const eliminatorForced = eliminatorValue.now(); + console.log("✅ Eliminator evaluated to:", eliminatorForced); + } + + console.log("Type-checking and evaluation through Source constructors successful!"); + } + } + + console.log("✅ MyNat datatype eliminator successfully executed!"); + }); + + it("should demonstrate complete integration: List datatype with high-level definition and low-level elimination", () => { + // Create initial context + const ctx: Context = new Map(); + + // Define simplified List datatype without parameterization to avoid scoping issues + const listDatatype = new DefineDatatypeSource( + testLoc, + "List", + [], // no parameters (simplified) + [], // no indices + [ + makeConstructorSpec("nil", []), + makeConstructorSpec("cons", []) // Simplified constructors + ] + ); + + // Handle the datatype definition + const result = handleDefineDatatype(ctx, new Map(), listDatatype); + expect(result).toBeInstanceOf(go); + if (result instanceof stop) { + throw new Error(`Failed to define List datatype: ${result.message}`); + } + + const updatedCtx = (result as go).result; - // it("should demonstrate Vector with indices", () => { - - // // Vec A n datatype - // const vecDatatype = new S.DefineDatatype( - // testLoc, - // "Vec", - // [new TypedBinder(new SiteBinder(testLoc, "A"), new S.Universe(testLoc))], // parameters - // [new TypedBinder(new SiteBinder(testLoc, "n"), new S.Nat(testLoc))], // indices - // new S.Universe(testLoc), - // [ - // // vnil : Vec A zero - // new S.ConstructorType( - // testLoc, - // "vnil", - // [], - // new S.Application( - // testLoc, - // new S.Name(testLoc, "Vec"), - // new S.Name(testLoc, "A"), - // [new S.Zero(testLoc)] - // ) - // ), - - // // vcons : (n : Nat) -> A -> Vec A n -> Vec A (add1 n) - // new S.ConstructorType( - // testLoc, - // "vcons", - // [ - // new TypedBinder(new SiteBinder(testLoc, "n"), new S.Nat(testLoc)), - // new TypedBinder(new SiteBinder(testLoc, "head"), new S.Name(testLoc, "A")), - // new TypedBinder(new SiteBinder(testLoc, "tail"), - // new S.Application(testLoc, new S.Name(testLoc, "Vec"), new S.Name(testLoc, "A"), [new S.Name(testLoc, "n")]) - // ) - // ], - // new S.Application( - // testLoc, - // new S.Name(testLoc, "Vec"), - // new S.Name(testLoc, "A"), - // [new S.Add1(testLoc, new S.Name(testLoc, "n"))] - // ) - // ) - // ] - // ); - - // // Using constructors: vcons 2 'a' (vcons 1 'b' (vcons 0 'c' vnil)) - // const vnil = new S.Constructor(testLoc, "vnil", []); - - // const vec1 = new S.Constructor( - // testLoc, - // "vcons", - // [ - // new S.Zero(testLoc), // n = 0 - // new S.Quote(testLoc, "c"), // head = 'c' - // vnil // tail = vnil - // ] - // ); - - // const vec2 = new S.Constructor( - // testLoc, - // "vcons", - // [ - // new S.Add1(testLoc, new S.Zero(testLoc)), // n = 1 - // new S.Quote(testLoc, "b"), // head = 'b' - // vec1 // tail = previous vec - // ] - // ); - - // // Test indexed structure - // expect(vecDatatype.indices).toHaveLength(1); - // expect(vecDatatype.indices[0].binder.varName).toBe("n"); - - // const vconsType = vecDatatype.constructors[1]; - // expect(vconsType.args).toHaveLength(3); // n, head, tail - // expect(vconsType.args[0].binder.varName).toBe("n"); - - // console.log("✅ Indexed Vec structure is correct!"); - // }); - + + // Verify components were added to context + expect(updatedCtx.has("List")).toBe(true); + expect(updatedCtx.has("nil")).toBe(true); + expect(updatedCtx.has("cons")).toBe(true); + expect(updatedCtx.has("elim-List")).toBe(true); + + // Use proper Source constructors for type-checking instead of creating Values directly + const nilSource = new S.ConstructorApplication(testLoc, "nil", []); + const consSource = new S.ConstructorApplication(testLoc, "cons", []); + + // Test type-checking through proper Source synthesis + const nilSynth = nilSource.synth(updatedCtx, new Map()); + const consSynth = consSource.synth(updatedCtx, new Map()); + + expect(nilSynth).toBeInstanceOf(go); + expect(consSynth).toBeInstanceOf(go); + + if (nilSynth instanceof go && consSynth instanceof go) { + // Verify the synthesized Core expressions + const nilCore = nilSynth.result.expr; + const consCore = consSynth.result.expr; + + expect(nilCore).toBeInstanceOf(C.Constructor); + expect(consCore).toBeInstanceOf(C.Constructor); + + if (nilCore instanceof C.Constructor && consCore instanceof C.Constructor) { + // Test that constructors have correct properties + expect(nilCore.name).toBe("nil"); + expect(consCore.name).toBe("cons"); + expect(nilCore.type).toBe("List"); + expect(consCore.type).toBe("List"); + expect(nilCore.index).toBe(0); + expect(consCore.index).toBe(1); + + // Test eliminator creation using Source constructors + const motiveSource = new S.Nat(testLoc); // Simple motive: List -> Nat + const method1Source = new S.Zero(testLoc); // nil -> 0 + const method2Source = new S.Add1(testLoc, new S.Zero(testLoc)); // cons -> 1 + + const listEliminatorSource = new S.EliminatorApplication( + testLoc, + "List", + nilSource, // target + motiveSource, // motive + [method1Source, method2Source] // methods + ); + + // Test that eliminator synthesis works through type-checking + const listEliminatorSynth = listEliminatorSource.synth(updatedCtx, new Map()); + expect(listEliminatorSynth).toBeInstanceOf(go); + + // ADD EVALUATION TESTS for List constructors + const nilValue = nilSynth.result.expr.valOf(contextToEnvironment(updatedCtx)); + const consValue = consSynth.result.expr.valOf(contextToEnvironment(updatedCtx)); + + // Verify the evaluated values + expect(nilValue).toBeInstanceOf(V.Constructor); + expect(consValue).toBeInstanceOf(V.Constructor); + + if (nilValue instanceof V.Constructor && consValue instanceof V.Constructor) { + expect(nilValue.name).toBe("nil"); + expect(consValue.name).toBe("cons"); + console.log("✅ List Evaluation: nil =", nilValue.name, "cons =", consValue.name); + } + + // Test eliminator evaluation + if (listEliminatorSynth instanceof go) { + const listEliminatorValue = listEliminatorSynth.result.expr.valOf(contextToEnvironment(updatedCtx)); + const listEliminatorForced = listEliminatorValue.now(); + console.log("✅ List Eliminator evaluated to:", listEliminatorForced); + } + + console.log("List type-checking and evaluation through Source constructors successful!"); + } + } + + console.log("✅ Complete List datatype integration successful!"); + }); + }); \ No newline at end of file diff --git a/src/pie_interpreter/__tests__/test_integration.ts b/src/pie_interpreter/__tests__/test_integration.ts new file mode 100644 index 00000000..dd965a69 --- /dev/null +++ b/src/pie_interpreter/__tests__/test_integration.ts @@ -0,0 +1,161 @@ +import 'jest'; +import * as S from '../types/source'; +import * as V from '../types/value'; +import * as C from '../types/core'; +import * as N from '../types/neutral'; +import * as Evaluator from '../evaluator/evaluator'; +import { Location, Syntax } from '../utils/locations'; +import { Position } from '../../scheme_parser/transpiler/types/location'; +import { DefineDatatypeSource, handleDefineDatatype, makeConstructorSpec, makeTypedBinder } from '../typechecker/definedatatype'; +import { Context, contextToEnvironment } from '../utils/context'; +import { go, stop, HigherOrderClosure, SiteBinder } from '../types/utils'; +import { Environment } from '../utils/environment'; +import { readBack } from '../evaluator/utils'; +import { prettyPrintValue } from '../unparser/pretty'; + +// Test location +const testLoc = new Location(new Syntax(new Position(1, 1), new Position(1, 1), 'test'), false); + + +describe( + 'test integration', () => { + + it("should create real recursive list structures like cons 1 (cons 2 (cons 3 nil))", () => { + const ctx: Context = new Map(); + const listDatatype = new DefineDatatypeSource( + testLoc, + "MyList", + [makeTypedBinder("E", new S.Universe(testLoc), testLoc)], + [], + [ + makeConstructorSpec("myNil", []), + makeConstructorSpec("myCons", [ + makeTypedBinder("head", new S.Name(testLoc, 'E'), testLoc), + makeTypedBinder("tail", new S.Name(testLoc, 'MyList'), testLoc) + ]) + ] + ); + + const result = handleDefineDatatype(ctx, new Map(), listDatatype); + const updatedCtx = (result as go).result; + + const nilSource = new S.ConstructorApplication(testLoc, "myNil", []); + + const three = new S.Add1(testLoc, new S.Add1(testLoc, new S.Add1(testLoc, new S.Zero(testLoc)))); + const cons3NilSource = new S.ConstructorApplication(testLoc, "myCons", [three, nilSource]); + + const two = new S.Add1(testLoc, new S.Add1(testLoc, new S.Zero(testLoc))); + const cons2Source = new S.ConstructorApplication(testLoc, "myCons", [two, cons3NilSource]); + + const one = new S.Add1(testLoc, new S.Zero(testLoc)); + const cons1Source = new S.ConstructorApplication(testLoc, "myCons", [one, cons2Source]); + + const nilSynth = nilSource.synth(updatedCtx, new Map()); + if (nilSynth instanceof go) { + const nilValue = nilSynth.result.expr.valOf(contextToEnvironment(updatedCtx)); + console.log(nilValue.prettyPrintValue()) + const cons1Synth = cons1Source.synth(updatedCtx, new Map()); + console.log("cons1Source synthesis result:", cons1Synth instanceof go ? "success" : "failed"); + } + const lengthNilSource = new S.EliminatorApplication( + testLoc, + "MyList", + nilSource, + new S.Nat(testLoc), + [ + new S.Zero(testLoc), + new S.Lambda(testLoc, new SiteBinder(testLoc, 'x'), new S.Add1()) + ] + ); + + const lengthNilSynth = lengthNilSource.synth(updatedCtx, new Map()); + expect(lengthNilSynth).toBeInstanceOf(go); + + if (lengthNilSynth instanceof go) { + // EVALUATE the length function on nil + const lengthNilValue = lengthNilSynth.result.expr.valOf(contextToEnvironment(updatedCtx)); + // Force evaluation of delayed values + const lengthNilForced = lengthNilValue.now(); + console.log("✅ Length of nil FORCED to:", lengthNilForced); + } + // Simple cons method for testing - returns 1 (will be enhanced later) + const consLengthMethod = new S.Add1(testLoc, new S.Zero(testLoc)); // returns 1 + + // First test: length of cons3NilSource (should be 1) + const lengthSingleConsSource = new S.EliminatorApplication( + testLoc, + "MyList", + cons3NilSource, // target: cons 3 nil (length should be 1) + new S.Nat(testLoc), // motive: List -> Nat + [ + new S.Zero(testLoc), // nil case: 0 + consLengthMethod // cons case: function that returns 1 + ] + ); + + // Simple recursive method for testing - returns 1 for now (will be enhanced to return add1(recursive_result)) + const consRecursiveLengthMethod = new S.Add1(testLoc, new S.Zero(testLoc)); // returns 1 + + // Second test: try to create a structure that gives length 3 + const lengthTripleConsSource = new S.EliminatorApplication( + testLoc, + "MyList", + cons1Source, // target: cons 1 (cons 2 (cons 3 nil)) - should give length 3 + new S.Nat(testLoc), // motive: List -> Nat + [ + new S.Zero(testLoc), // nil case: 0 + consRecursiveLengthMethod // cons case: λ(element tail tail_length) add1(tail_length) + ] + ); + + // Test the single cons first + try { + const singleSynth = lengthSingleConsSource.synth(updatedCtx, new Map()); + if (singleSynth instanceof go) { + const singleValue = singleSynth.result.expr.valOf(contextToEnvironment(updatedCtx)); + const singleForced = singleValue.now(); + console.log("✅ Single cons (cons 3 nil) length evaluates to:", singleForced); + + if (singleForced instanceof V.Add1) { + const base = singleForced.smaller.now(); + if (base instanceof V.Zero) { + console.log("✅ SUCCESS: Single cons correctly gives length 1!"); + } + } + } + } catch (e) { + console.log("Single cons length failed:", e.message); + } + + // Test the triple nested cons + try { + const tripleSynth = lengthTripleConsSource.synth(updatedCtx, new Map()); + if (tripleSynth instanceof go) { + const tripleValue = tripleSynth.result.expr.valOf(contextToEnvironment(updatedCtx)); + const tripleForced = tripleValue.now(); + console.log("✅ Triple cons (cons 1 (cons 2 (cons 3 nil))) length evaluates to:", tripleForced); + + // Check if we got 3: Add1(Add1(Add1(Zero))) + if (tripleForced instanceof V.Add1) { + const second = tripleForced.smaller.now(); + if (second instanceof V.Add1) { + const third = second.smaller.now(); + if (third instanceof V.Add1) { + const base = third.smaller.now(); + if (base instanceof V.Zero) { + console.log("✅ SUCCESS: Triple nested cons correctly gives length 3!"); + return; // Success! + } + } + } + } + console.log("❌ Triple cons didn't give expected length 3 structure"); + } + } catch (e) { + console.log("Triple cons length failed:", e.message); + } + + }); + + } +) \ No newline at end of file diff --git a/src/pie_interpreter/__tests__/test_telescope.ts b/src/pie_interpreter/__tests__/test_telescope.ts new file mode 100644 index 00000000..27324ecd --- /dev/null +++ b/src/pie_interpreter/__tests__/test_telescope.ts @@ -0,0 +1,10 @@ +import 'jest' +import { evaluatePie } from '../main'; + +describe('test_telescope', () => { + it('test0', () => + console.log(evaluatePie( + ` + (claim test (Pi ((A U) (x A)) A))` + ))) +}) \ No newline at end of file diff --git a/src/pie_interpreter/evaluator/evaluator.ts b/src/pie_interpreter/evaluator/evaluator.ts index d9f1013b..13f36ee1 100644 --- a/src/pie_interpreter/evaluator/evaluator.ts +++ b/src/pie_interpreter/evaluator/evaluator.ts @@ -782,8 +782,8 @@ export function doEliminator(name: string, target: V.Value, motive: V.Value, met // Check if target is a constructor application of the inductive type if (targetNow instanceof V.Constructor) { - if (targetNow.name != name) { - throw new Error(`doEliminator: wrong eliminator used. Got: ${targetNow.name}; Expected: ${name}`); + if (targetNow.type != name) { + throw new Error(`doEliminator: wrong eliminator used. Got constructor of type: ${targetNow.type}; Expected: ${name}`); } const constructorIndex = targetNow.index; if (constructorIndex >= 0 && constructorIndex < methods.length) { diff --git a/src/pie_interpreter/typechecker/definedatatype.ts b/src/pie_interpreter/typechecker/definedatatype.ts index 0f3c3821..d8d4c276 100644 --- a/src/pie_interpreter/typechecker/definedatatype.ts +++ b/src/pie_interpreter/typechecker/definedatatype.ts @@ -1,68 +1,127 @@ import * as S from '../types/source'; import * as C from '../types/core'; import * as V from '../types/value'; -import { go, goOn, Perhaps, stop, fresh, TypedBinder, Message } from '../types/utils'; -import { Context, extendContext, getInductiveType, InductiveDatatypePlaceholder, InductiveDatatypeBinder, ConstructorBinder, contextToEnvironment, EliminatorBinder, valInContext } from '../utils/context'; +import { go, Perhaps, stop, fresh, TypedBinder, Message, SiteBinder, HigherOrderClosure } from '../types/utils'; +import { Context, extendContext, InductiveDatatypePlaceholder, InductiveDatatypeBinder, ConstructorBinder, contextToEnvironment, EliminatorBinder, valInContext, bindFree } from '../utils/context'; import { Location } from '../utils/locations'; -import { rename, Renaming } from './utils'; -import { Constructor } from '../types/value'; +import { Renaming } from './utils'; import { Environment } from '../utils/environment'; +function isRecursiveArgumentType(argType: S.Source, datatypeName: string): boolean { + // Check for direct name reference + if (argType instanceof S.Name && argType.name === datatypeName) { + return true; + } + + // Check for application with datatype name as function + if (argType instanceof S.Application && + argType.func instanceof S.Name && + argType.func.name === datatypeName) { + return true; + } + + // Check for string representation (fallback to original logic) + const typePrint = argType.prettyPrint(); + return typePrint === datatypeName || typePrint.includes(datatypeName); +} + +export interface ConstructorSpec { + name: string; + args: TypedBinder[]; +} + export class DefineDatatypeSource { constructor( public location: Location, public name: string, - public parameters: S.The[], - public indices: S.The[], - public constructors: { name: string, args: S.The[] }[], - public typeValue: V.Value + public parameters: TypedBinder[], + public indices: TypedBinder[], + public constructors: ConstructorSpec[], + public eliminatorName?: string ) { } public toString(): string { - return `data ${this.name} ${this.parameters.map(p => p.toString()).join(' ')} where ${this.constructors.map(c => c.name + ' ' + c.args.map(a => a.toString()).join(' ')).join(', ')}`; + const params = this.parameters.map(p => p.prettyPrint()).join(' '); + const indices = this.indices.map(i => i.prettyPrint()).join(' '); + const ctors = this.constructors.map(c => + `${c.name} ${c.args.map(a => a.prettyPrint()).join(' ')}` + ).join(', '); + return `data ${this.name} (${params}) (${indices}) ${ctors}`; } public typeSynth(ctx: Context, rename: Renaming): Perhaps { - const synthedParameters = this.parameters.map(p => p.type.isType(ctx, rename)) - .map(p => { - if (p instanceof stop) { - throw new Error(`Parameter type is not a type at ${p.where}`) - } - return (p as go).result - }) - const synthedIndices = this.indices.map(p => p.type.isType(ctx, rename)) - .map(p => { - if (p instanceof stop) { - throw new Error(`Index type is not a type at ${p.where}`) - } - return (p as go).result - }) - + let currentCtx = ctx; + const synthedParameters: C.Core[] = []; + + for (const param of this.parameters) { + const paramTypeResult = param.type.isType(currentCtx, rename); + if (paramTypeResult instanceof stop) { + return new stop(param.binder.location, new Message([`Parameter type is not a type: ${paramTypeResult.message}`])); + } + + const paramTypeCore = (paramTypeResult as go).result; + synthedParameters.push(paramTypeCore); + + // Extend context with this parameter for subsequent parameters and indices + currentCtx = bindFree(currentCtx, param.binder.varName, valInContext(currentCtx, paramTypeCore)); + } + + // 2. Type check indices in extended context (can reference parameters) + const synthedIndices: C.Core[] = []; + + for (const index of this.indices) { + const indexTypeResult = index.type.isType(currentCtx, rename); + if (indexTypeResult instanceof stop) { + return new stop(index.binder.location, new Message([`Index type is not a type: ${indexTypeResult.message}`])); + } + + const indexTypeCore = (indexTypeResult as go).result; + synthedIndices.push(indexTypeCore); + + // Extend context with this index for subsequent indices and constructors + currentCtx = bindFree(currentCtx, index.binder.varName, valInContext(currentCtx, indexTypeCore)); + } + + // 3. Type check constructors in fully extended context let counter = 0; - const synthedConstructors = this.constructors.map( - p => { - const typecheckedArgs = p.args.map(arg => arg.isType(ctx, rename)) - .map(arg => { - if (arg instanceof stop) { - throw new Error(`Constructor argument type is not a type at ${arg.where}`) - } - return (arg as go).result - }) - - // Find recursive arguments (those with type T) - const coreRecArgs = p.args.filter(arg => - arg.prettyPrint().includes(this.name) - ).map(arg => arg.isType(ctx, rename)) - .map(arg => { - if (arg instanceof stop) { - throw new Error(`Recursive argument type is not a type at ${arg.where}`) - } - return (arg as go).result - }) - return new C.Constructor(p.name, this.name, typecheckedArgs, counter++, coreRecArgs) + const synthedConstructors: C.Constructor[] = []; + + for (const ctor of this.constructors) { + const result = this.typeCheckConstructor(currentCtx, rename, ctor, counter++); + if (result instanceof stop) { + return result; } - ) - return new go(new DefineDatatypeCore(this.name, synthedParameters, synthedIndices, synthedConstructors)) + synthedConstructors.push((result as go).result); + } + + return new go(new DefineDatatypeCore(this.name, synthedParameters, synthedIndices, synthedConstructors)); + } + + private typeCheckConstructor(ctx: Context, rename: Renaming, ctor: ConstructorSpec, index: number): Perhaps { + // Type check constructor arguments in sequence, extending context + let currentCtx = ctx; + const typecheckedArgs: C.Core[] = []; + const coreRecArgs: C.Core[] = []; + + for (const arg of ctor.args) { + const argTypeResult = arg.type.isType(currentCtx, rename); + if (argTypeResult instanceof stop) { + return new stop(arg.binder.location, new Message([`Constructor argument type is not a type: ${argTypeResult.message}`])); + } + + const argTypeCore = (argTypeResult as go).result; + typecheckedArgs.push(argTypeCore); + + // Check if this argument type refers to the datatype being defined (recursive) + if (isRecursiveArgumentType(arg.type, this.name)) { + coreRecArgs.push(argTypeCore); + } + + // Extend context with this argument for subsequent arguments + currentCtx = bindFree(currentCtx, arg.binder.varName, valInContext(currentCtx, argTypeCore)); + } + + return new go(new C.Constructor(ctor.name, this.name, typecheckedArgs, index, coreRecArgs)); } } @@ -161,42 +220,63 @@ export class EliminatorGenerator { } export function handleDefineDatatype(ctx: Context, renaming: Renaming, target: DefineDatatypeSource): Perhaps { - const placeholder = new InductiveDatatypePlaceholder(target.name) if (ctx.has(target.name)) { - throw new Error(`this name is already in use ${target.name}`) + return new stop(target.location, new Message([`Name already in use: ${target.name}`])); } - extendContext(ctx, target.name, placeholder) - - const synthesized = target.typeSynth(ctx, renaming) + + // Create placeholder - for parameterized types, make it a function + const placeholder = new InductiveDatatypePlaceholder(target.name); + + if (target.parameters.length > 0) { + // For parameterized types like List, create: (E : U) -> U + // Use HigherOrderClosure to avoid variable reference issues + let resultType: V.Value = new V.Universe(); + + for (let i = target.parameters.length - 1; i >= 0; i--) { + const paramName = target.parameters[i].binder.varName; + resultType = new V.Pi( + paramName, + new V.Universe(), + new HigherOrderClosure((_arg: V.Value) => new V.Universe()) + ); + } + + placeholder.type = resultType; + } + + let cur_ctx = extendContext(ctx, target.name, placeholder) + + const synthesized = target.typeSynth(cur_ctx, renaming) if (synthesized instanceof stop) { return synthesized } const core = (synthesized as go).result - ctx.delete(target.name) + cur_ctx.delete(target.name) // 1. Add the datatype itself - extendContext(ctx, core.name, new InductiveDatatypeBinder(core.name, core.valOf(contextToEnvironment(ctx)))) + cur_ctx = extendContext(cur_ctx, core.name, new InductiveDatatypeBinder(core.name, core.valOf(contextToEnvironment(cur_ctx)))) - // 2. Add each constructor + // 2. Add each constructor for (const ctor of core.constructors) { - extendContext(ctx, ctor.name, new ConstructorBinder(ctor.name, ctor.valOf(contextToEnvironment(ctx)))) + cur_ctx = extendContext(cur_ctx, ctor.name, new ConstructorBinder(ctor.name, ctor.valOf(contextToEnvironment(cur_ctx)))) } - // 3. Generate and add the eliminator (following the algorithm) - const eliminatorName = `elim${core.name}`; + // 3. Generate and add the eliminator + const eliminatorName = target.eliminatorName || `elim${core.name}`; const eliminatorGenerator = new EliminatorGenerator( eliminatorName, core.name, - core.parameters, + core.parameters, core.indices, core.constructors ); // Add eliminator to context - extendContext(ctx, eliminatorName, new EliminatorBinder(eliminatorName, valInContext(ctx, eliminatorGenerator.generateEliminatorType(ctx)))); + const eliminatorType = eliminatorGenerator.generateEliminatorType(cur_ctx); + cur_ctx = extendContext(cur_ctx, eliminatorName, new EliminatorBinder(eliminatorName, valInContext(cur_ctx, eliminatorType))); - return new go(ctx) + return new go(cur_ctx) } // Type synthesis for eliminator applications @@ -210,7 +290,6 @@ export function synthEliminator( methods: S.Source[] ): Perhaps { - // Get eliminator from context const elimBinder = ctx.get(elimName); if (!elimBinder || !(elimBinder instanceof EliminatorGenerator)) { return new stop(location, new Message([`Unknown eliminator: ${elimName}`])); @@ -250,7 +329,76 @@ export function synthEliminator( elimBinder.datatypeName, (targetSynth as go).result.expr, (motiveSynth as go).result.expr, - methods.map((m, i) => ((m.synth(ctx, renaming) as go).result.expr)) + methods.map(m => ((m.synth(ctx, renaming) as go).result.expr)) ) )); +} + +// Helper functions for creating inductive types with TypedBinder + +export function makeTypedBinder(name: string, type: S.Source, location: Location): TypedBinder { + return new TypedBinder(new SiteBinder(location, name), type); +} + +export function makeConstructorSpec(name: string, args: TypedBinder[]): ConstructorSpec { + return { name, args}; +} + +// Example factory functions for common inductive types + +export function createListDatatype(location: Location): DefineDatatypeSource { + const elemParam = makeTypedBinder("E", new S.Universe(location), location); + + return new DefineDatatypeSource( + location, + "List", + [elemParam], // Type parameters: ((E U)) + [], // No indices + [ + makeConstructorSpec("nil", []), + makeConstructorSpec("::", [ + makeTypedBinder("head", new S.Name(location, "E"), location), + makeTypedBinder("tail", new S.Application(location, new S.Name(location, "List"), new S.Name(location, "E"), []), location) + ]) + ], + "ind-List" // Eliminator name + ); +} + +export function createVecDatatype(location: Location): DefineDatatypeSource { + const elemParam = makeTypedBinder("E", new S.Universe(location), location); + const lengthIndex = makeTypedBinder("n", new S.Nat(location), location); + + return new DefineDatatypeSource( + location, + "Vec", + [elemParam], // Type parameters: ((E U)) + [lengthIndex], // Index parameters: ((n Nat)) + [ + makeConstructorSpec("vnil", [], + // Explicit result type: (Vec E zero) + new S.Application(location, + new S.Application(location, new S.Name(location, "Vec"), new S.Name(location, "E"), []), + new S.Zero(location), [] + ) + ), + makeConstructorSpec("vcons", [ + makeTypedBinder("head", new S.Name(location, "E"), location), + makeTypedBinder("tail", + new S.Application(location, + new S.Application(location, new S.Name(location, "Vec"), new S.Name(location, "E"), []), + new S.Name(location, "n"), [] + ), + location + ) + ], + // Explicit result type: (Vec E (add1 n)) + new S.Application(location, + new S.Application(location, new S.Name(location, "Vec"), new S.Name(location, "E"), []), + new S.Add1(location, new S.Name(location, "n")), [] + ) + ) + ], + "ind-Vec" // Eliminator name + ); } \ No newline at end of file diff --git a/src/pie_interpreter/types/source.ts b/src/pie_interpreter/types/source.ts index dcc87b1c..088e7e67 100644 --- a/src/pie_interpreter/types/source.ts +++ b/src/pie_interpreter/types/source.ts @@ -5,7 +5,7 @@ import * as S from './source'; import { PieInfoHook, Renaming, SendPieInfo, extendRenaming, makeApp, rename} from '../typechecker/utils'; import { Location, notForInfo } from '../utils/locations'; -import { bindFree, Context, readBackContext, valInContext } from '../utils/context'; +import { bindFree, Context, readBackContext, valInContext, getInductiveType, InductiveDatatypeBinder, ConstructorBinder, EliminatorBinder, contextToEnvironment } from '../utils/context'; import { go, stop, goOn, occurringBinderNames, Perhaps, PerhapsM, SiteBinder, TypedBinder, Message, freshBinder, @@ -2006,34 +2006,115 @@ export class ConstructorType extends Source { } -export class Constructor extends Source { - protected synthHelper(ctx: Context, renames: Renaming): Perhaps { - throw new Error('Method not implemented.'); +// Constructor expression - references a constructor by name and applies it to arguments +// Helper function to check if an argument is a recursive reference +function isArgumentRecursive(arg: Source, datatypeName: string, ctx: Context, renames: Renaming): boolean { + try { + const argSynth = arg.synth(ctx, renames); + if (argSynth instanceof go) { + const argType = argSynth.result.type; + return isTypeReference(argType, datatypeName, ctx); + } + } catch (e) { + // If synthesis fails, assume not recursive + } + return false; +} + +// Helper function to check if a Core type refers to a specific datatype +function isTypeReference(typeCore: C.Core, datatypeName: string, ctx: Context): boolean { + if (typeCore instanceof C.VarName && typeCore.name === datatypeName) { + return true; } + if (typeCore instanceof C.InductiveType && typeCore.typeName === datatypeName) { + return true; + } + // For more complex cases, we could evaluate the type and check + try { + const typeValue = typeCore.valOf(contextToEnvironment(ctx)); + if (typeValue instanceof V.InductiveType && typeValue.name === datatypeName) { + return true; + } + } catch (e) { + // If evaluation fails, continue with other checks + } + return false; +} + +export class ConstructorApplication extends Source { constructor( public location: Location, - public name: string, - public args: Source[], // Constructor args - public resultType: Source // Type the constructor produces + public constructorName: string, + public args: Source[] // Arguments to apply to constructor ) { super(location); } + protected synthHelper(ctx: Context, renames: Renaming): Perhaps { + // Look up constructor in context + const constructorBinder = ctx.get(this.constructorName); + if (!constructorBinder || !(constructorBinder instanceof ConstructorBinder)) { + return new stop(this.location, new Message([`Unknown constructor: ${this.constructorName}`])); + } + + const constructorType = constructorBinder.type; + + // Check arguments against constructor type + const checkedArgs: C.Core[] = []; + + // For now, simplified: assume constructor takes any number of args + // In a full implementation, we'd check each arg against the constructor's expected types + for (const arg of this.args) { + const argResult = arg.synth(ctx, renames); + if (argResult instanceof stop) { + return argResult; + } + checkedArgs.push((argResult as go).result.expr); + } + + // Properly categorize recursive vs non-recursive arguments + const recursiveArgs: C.Core[] = []; + for (let i = 0; i < this.args.length; i++) { + if (isArgumentRecursive(this.args[i], constructorType.type, ctx, renames)) { + recursiveArgs.push(checkedArgs[i]); + } + } + + // Create Core constructor application + const constructorCore = new C.Constructor( + this.constructorName, // constructor name (e.g., "true") + constructorType.type, // type name (e.g., "Bool") + checkedArgs, // all arguments + constructorType.index, + recursiveArgs // only recursive arguments + ); + + // Return The with constructor application and its type + // Note: C.The constructor is (type: Core, expr: Core) + return new go(new C.The( + new C.InductiveType( + constructorType.type, + [], // simplified - no parameters for now + [] // simplified - no indices for now + ), + constructorCore + )); + } + public findNames(): string[] { - const names = [this.name]; + const names = [this.constructorName]; names.push(...this.args.flatMap(a => a.findNames())); - names.push(...this.resultType.findNames()); return names; } public prettyPrint(): string { - const args = this.args.map(a => `[${a.prettyPrint()}]`).join(' '); - return `[${this.name} ${args} : ${this.resultType.prettyPrint()}]`; + const args = this.args.map(a => a.prettyPrint()).join(' '); + return `(${this.constructorName}${args.length > 0 ? ' ' + args : ''})`; } } // Generic eliminator for user-defined inductive types -export class GenericEliminator extends Source { +export class EliminatorApplication extends Source { constructor( public location: Location, public typeName: string, @@ -2043,7 +2124,61 @@ export class GenericEliminator extends Source { ) { super(location); } protected synthHelper(ctx: Context, renames: Renaming): Perhaps { - throw new Error('Method not implemented.'); + // Look up the inductive type in context + const inductiveTypeBinder = getInductiveType(ctx, this.location, this.typeName); + if (inductiveTypeBinder instanceof stop) { + return inductiveTypeBinder; + } + + const inductiveType = (inductiveTypeBinder as go).result.type; + + // Look up the eliminator in context + const eliminatorName = `elim${this.typeName}`; + const eliminatorBinder = ctx.get(eliminatorName); + if (!eliminatorBinder || !(eliminatorBinder instanceof EliminatorBinder)) { + return new stop(this.location, new Message([`Unknown eliminator: ${eliminatorName}`])); + } + + // Check target against inductive type + const targetResult = this.target.synth(ctx, renames); + if (targetResult instanceof stop) { + return targetResult; + } + + const targetCore = (targetResult as go).result; + + // Check motive + const motiveResult = this.motive.synth(ctx, renames); + if (motiveResult instanceof stop) { + return motiveResult; + } + + const motiveCore = (motiveResult as go).result; + + // Check methods + const checkedMethods: C.Core[] = []; + for (const method of this.methods) { + const methodResult = method.synth(ctx, renames); + if (methodResult instanceof stop) { + return methodResult; + } + checkedMethods.push((methodResult as go).result.expr); + } + + // Create Core eliminator application + const eliminatorCore = new C.Eliminator( + this.typeName, + targetCore.expr, + motiveCore.expr, + checkedMethods + ); + + // The result type depends on the motive applied to the target + // For now, simplified - in a full implementation we'd compute the proper result type + const resultType = new C.Application(motiveCore.expr, targetCore.expr); + + // Note: C.The constructor is (type: Core, expr: Core) + return new go(new C.The(resultType, eliminatorCore)); } public findNames(): string[] { diff --git a/src/pie_interpreter/utils/context.ts b/src/pie_interpreter/utils/context.ts index 7f342e42..9c0b7508 100644 --- a/src/pie_interpreter/utils/context.ts +++ b/src/pie_interpreter/utils/context.ts @@ -129,6 +129,8 @@ export function contextToEnvironment(ctx: Context): Environment { env.set(name, binder.value); } else if (binder instanceof Free) { env.set(name, new Neutral(binder.type, new Variable(name))); + } else if (binder instanceof InductiveDatatypePlaceholder) { + env.set(name, new Neutral(binder.type, new Variable(name))); } // else continue; } return env; From b2c3fcb64780a60ece4fdbcc4e72d98657302c0f Mon Sep 17 00:00:00 2001 From: ZhangQixiang123 Date: Sun, 21 Sep 2025 21:57:39 -0700 Subject: [PATCH 05/10] reuse PI --- src/language_server/package.json | 130 ++++++++++++++++++ .../typechecker/definedatatype.ts | 117 +++++++++++++--- 2 files changed, 229 insertions(+), 18 deletions(-) create mode 100644 src/language_server/package.json diff --git a/src/language_server/package.json b/src/language_server/package.json new file mode 100644 index 00000000..95739536 --- /dev/null +++ b/src/language_server/package.json @@ -0,0 +1,130 @@ +{ + "name": "pie-lsp", + "description": "A language server for Pie", + "author": "Ding Feng, Li Daoxin, Zhang Qixiang", + "publisher": "source-academy", + "version": "1.0.0", + "repository": { + "type": "git" + }, + "categories": [], + "keywords": [ + "multi-root ready" + ], + "engines": { + "vscode": "^1.103.0" + }, + "activationEvents": [ + "onLanguage:pie" + ], + "main": "./out/src/language_server/client/src/extension", + "contributes": { + "languages": [ + { + "id": "pie", + "aliases": [ + "Pie", + "pie" + ], + "extensions": [ + ".pie" + ], + "configuration": "./language-configuration.json" + } + ], + "grammars": [ + { + "language": "pie", + "scopeName": "source.pie", + "path": "./syntaxes/pie.tmLanguage.json" + } + ], + "views": { + "explorer": [ + { + "id": "pieOutput", + "name": "Pie Output" + } + ] + }, + "commands": [ + { + "command": "pie.runCode", + "title": "Run Pie Code", + "icon": "$(play)" + }, + { + "command": "pie.refreshOutput", + "title": "Refresh", + "icon": "$(refresh)" + } + ], + "menus": { + "editor/title": [ + { + "command": "pie.runCode", + "when": "resourceExtname == .pie", + "group": "navigation" + } + ], + "view/title": [ + { + "command": "pie.refreshOutput", + "when": "view == pieOutput", + "group": "navigation" + } + ] + }, + "configuration": { + "type": "object", + "title": "Example configuration", + "properties": { + "languageServerExample.maxNumberOfProblems": { + "scope": "resource", + "type": "number", + "default": 100, + "description": "Controls the maximum number of problems produced by the server." + }, + "languageServerExample.trace.server": { + "scope": "window", + "type": "string", + "enum": [ + "off", + "messages", + "verbose" + ], + "default": "off", + "description": "Traces the communication between VS Code and the language server." + } + } + } + }, + "scripts": { + "vscode:prepublish": "npm run compile", + "compile": "tsc || true", + "watch": "tsc -w", + "lint": "eslint", + "test": "jest", + "clean": "rimraf out" + }, + "dependencies": { + "@types/estree": "^1.0.8", + "js-base64": "^3.7.8", + "vscode-languageclient": "^9.0.1", + "vscode-languageserver": "^9.0.1", + "vscode-languageserver-textdocument": "^1.0.11" + }, + "devDependencies": { + "@eslint/js": "^9.13.0", + "@stylistic/eslint-plugin": "^2.9.0", + "@types/jest": "^29.5.14", + "@types/node": "^22", + "@types/vscode": "^1.103.0", + "eslint": "^9.13.0", + "jest": "^29.7.0", + "rimraf": "^3.0.2", + "ts-jest": "^29.4.1", + "typescript": "^5.9.2", + "typescript-eslint": "^8.39.0" + } +} \ No newline at end of file diff --git a/src/pie_interpreter/typechecker/definedatatype.ts b/src/pie_interpreter/typechecker/definedatatype.ts index d8d4c276..7d43dbc2 100644 --- a/src/pie_interpreter/typechecker/definedatatype.ts +++ b/src/pie_interpreter/typechecker/definedatatype.ts @@ -2,32 +2,50 @@ import * as S from '../types/source'; import * as C from '../types/core'; import * as V from '../types/value'; import { go, Perhaps, stop, fresh, TypedBinder, Message, SiteBinder, HigherOrderClosure } from '../types/utils'; -import { Context, extendContext, InductiveDatatypePlaceholder, InductiveDatatypeBinder, ConstructorBinder, contextToEnvironment, EliminatorBinder, valInContext, bindFree } from '../utils/context'; +import { Context, extendContext, InductiveDatatypePlaceholder, InductiveDatatypeBinder, ConstructorBinder, contextToEnvironment, EliminatorBinder, valInContext, bindFree, getClaim } from '../utils/context'; import { Location } from '../utils/locations'; -import { Renaming } from './utils'; +import { extendRenaming, Renaming } from './utils'; import { Environment } from '../utils/environment'; +import { VarName } from '../types/core'; +import { synthesizer } from './synthesizer'; function isRecursiveArgumentType(argType: S.Source, datatypeName: string): boolean { - // Check for direct name reference if (argType instanceof S.Name && argType.name === datatypeName) { return true; } - // Check for application with datatype name as function if (argType instanceof S.Application && - argType.func instanceof S.Name && + argType.func instanceof generalInductiveType && argType.func.name === datatypeName) { return true; } - // Check for string representation (fallback to original logic) - const typePrint = argType.prettyPrint(); - return typePrint === datatypeName || typePrint.includes(datatypeName); + return false; } -export interface ConstructorSpec { - name: string; - args: TypedBinder[]; +export class generalInductiveType extends S.Source { + public findNames(): string[] { + throw new Error('Method not implemented.'); + } + public prettyPrint(): string { + throw new Error('Method not implemented.'); + } + protected synthHelper(ctx: Context, renames: Renaming): Perhaps { + const resultTemp = getClaim(ctx, this.location, this.name) + if (resultTemp instanceof stop) { + return resultTemp + } + + const result = (resultTemp as go).result + return result.readBackType(ctx) + } + constructor( + public location: Location, + public name: string, + args: SiteBinder + ) {super(location)} + + } export class DefineDatatypeSource { @@ -35,20 +53,82 @@ export class DefineDatatypeSource { public location: Location, public name: string, public parameters: TypedBinder[], - public indices: TypedBinder[], - public constructors: ConstructorSpec[], + public indices: S.Pi, + public constructors: S.Pi[], public eliminatorName?: string ) { } public toString(): string { const params = this.parameters.map(p => p.prettyPrint()).join(' '); - const indices = this.indices.map(i => i.prettyPrint()).join(' '); - const ctors = this.constructors.map(c => - `${c.name} ${c.args.map(a => a.prettyPrint()).join(' ')}` - ).join(', '); + const indices = this.indices.prettyPrint(); + const ctors = this.constructors.map(p => p.prettyPrint()).join(' '); return `data ${this.name} (${params}) (${indices}) ${ctors}`; } + // checkOneType(ctx: Context, rename: Renaming, binder: SiteBinder, type:S.Source) { + // const xhat = fresh(ctx, binder.varName) + // const result = type.check(ctx, rename, new V.Universe()) + // if (result instanceof go) { + // return new go( + // new ContextAndRenaming( + // bindFree(ctx, xhat, valInContext(ctx, result.result)), + // extendRenaming(rename, binder.varName, xhat) + // )) + // } else { + // throw (result as stop).message + // } + // } + + // checkParams(ctx: Context, rename:Renaming) { + // let cur_ctx = ctx; + // let cur_rename = rename + // for (const param of this.parameters) { + // const result = this.checkOneType(cur_ctx, cur_rename, param.binder, param.type) + // if (result instanceof go) { + // const cur_result= (result as go).result + // cur_ctx = cur_result.ctx + // cur_rename = cur_result.rename + // } else { + // throw (result as stop).message + // } + // } + // return new go(new ContextAndRenaming(cur_ctx, cur_rename)) + // } + + // synthIndices(ctx: Context, rename:Renaming) { + // return this.indices.synth(ctx, rename) + // } + + buildMainTypeAndConstructor(ctx: Context, rename:Renaming) { + const mainTypeTemp = new S.Pi(this.location, this.parameters, this.indices).getType(ctx, rename) + if (mainTypeTemp instanceof stop) { + return mainTypeTemp + } + const namehat = fresh(ctx, this.name) + let cur_ctx = bindFree(ctx, namehat, + valInContext(ctx, (mainTypeTemp as go).result) + ) + let cur_rename = extendRenaming(rename, this.name, namehat) + + let constructorls = this.constructors.map( + ctor => ctor.synth(cur_ctx, cur_rename) + ) + } + + findAllRecTypes(ctor:S.Pi, acc: string[]) { + + } + + handleConstructor(ctx:Context, rename:Renaming, ctor:S.Pi) { + + } + + + + + + + public typeSynth(ctx: Context, rename: Renaming): Perhaps { let currentCtx = ctx; const synthedParameters: C.Core[] = []; @@ -401,4 +481,5 @@ export function createVecDatatype(location: Location): DefineDatatypeSource { ], "ind-Vec" // Eliminator name ); -} \ No newline at end of file +} + From 65add1bcb1f06a4b1399723bbb860d7fc49fbd60 Mon Sep 17 00:00:00 2001 From: ZhangQixiang123 Date: Wed, 15 Oct 2025 11:09:59 +0800 Subject: [PATCH 06/10] inductive type without parser --- dist/index.js | 2 +- dist/index.js.map | 2 +- .../__tests__/test_definedatatype.ts | 761 ++++++++++++++++++ .../__tests__/test_doEliminator_core.ts | 32 +- .../__tests__/test_inductive_design.ts | 486 ----------- .../__tests__/test_integration.ts | 161 ---- src/pie_interpreter/__tests__/test_lsp.pie | 9 + .../__tests__/test_method_type.ts | 148 ++++ .../__tests__/test_motive_type.ts | 126 +++ .../__tests__/test_normalize_constructor.ts | 391 +++++++++ src/pie_interpreter/evaluator/evaluator.ts | 2 +- .../typechecker/definedatatype.ts | 716 +++++++--------- .../typechecker/synthesizer.ts | 606 ++++++++++---- src/pie_interpreter/types/core.ts | 54 +- src/pie_interpreter/types/source.ts | 345 ++++---- src/pie_interpreter/types/utils.ts | 2 +- src/pie_interpreter/types/value.ts | 79 +- src/pie_interpreter/utils/alphaeqv.ts | 12 + src/pie_interpreter/utils/context.ts | 25 +- test_eliminator_simple.ts | 90 +++ 20 files changed, 2570 insertions(+), 1479 deletions(-) create mode 100644 src/pie_interpreter/__tests__/test_definedatatype.ts delete mode 100644 src/pie_interpreter/__tests__/test_inductive_design.ts delete mode 100644 src/pie_interpreter/__tests__/test_integration.ts create mode 100644 src/pie_interpreter/__tests__/test_lsp.pie create mode 100644 src/pie_interpreter/__tests__/test_method_type.ts create mode 100644 src/pie_interpreter/__tests__/test_motive_type.ts create mode 100644 src/pie_interpreter/__tests__/test_normalize_constructor.ts create mode 100644 test_eliminator_simple.ts diff --git a/dist/index.js b/dist/index.js index 1fcb0e47..4bf32ce3 100644 --- a/dist/index.js +++ b/dist/index.js @@ -1,2 +1,2 @@ -!function(){"use strict";class t extends Error{name="ConductorError";errorType="__unknown";constructor(t){super(t)}}class e extends t{name="ConductorInternalError";errorType="__internal";constructor(t){super(t)}}class n{conductor;async startEvaluator(t){const n=await this.conductor.requestFile(t);if(!n)throw new e("Cannot load entrypoint file");for(await this.evaluateFile(t,n);;){const t=await this.conductor.requestChunk();await this.evaluateChunk(t)}}async evaluateFile(t,e){return this.evaluateChunk(e)}constructor(t){this.conductor=t}}async function r(t){return(await import(t)).plugin}"function"==typeof SuppressedError&&SuppressedError;class s{name;__port;__subscribers=new Set;__isAlive=!0;__waitingMessages=[];send(t,e){this.__verifyAlive(),this.__port.postMessage(t,e??[])}subscribe(t){if(this.__verifyAlive(),this.__subscribers.add(t),this.__waitingMessages){for(const e of this.__waitingMessages)t(e);delete this.__waitingMessages}}unsubscribe(t){this.__verifyAlive(),this.__subscribers.delete(t)}close(){this.__verifyAlive(),this.__isAlive=!1,this.__port?.close()}__verifyAlive(){if(!this.__isAlive)throw new e(`Channel ${this.name} has been closed`)}__dispatch(t){if(this.__verifyAlive(),this.__waitingMessages)this.__waitingMessages.push(t);else for(const e of this.__subscribers)e(t)}listenToPort(t){t.addEventListener("message",(t=>this.__dispatch(t.data))),t.start()}replacePort(t){this.__verifyAlive(),this.__port?.close(),this.__port=t,this.listenToPort(t)}constructor(t,e){this.name=t,this.replacePort(e)}}class i{__s1=[];__s2=[];push(t){this.__s2.push(t)}pop(){if(0===this.__s1.length){if(0===this.__s2.length)throw new Error("queue is empty");let t=this.__s1;this.__s1=this.__s2.reverse(),this.__s2=t}return this.__s1.pop()}get length(){return this.__s1.length+this.__s2.length}clone(){const t=new i;return t.__s1=[...this.__s1],t.__s2=[...this.__s2],t}}class a{__inputQueue=new i;__promiseQueue=new i;push(t){0!==this.__promiseQueue.length?this.__promiseQueue.pop()(t):this.__inputQueue.push(t)}async pop(){return 0!==this.__inputQueue.length?this.__inputQueue.pop():new Promise(((t,e)=>{this.__promiseQueue.push(t)}))}tryPop(){if(0!==this.__inputQueue.length)return this.__inputQueue.pop()}constructor(){this.push=this.push.bind(this)}}class o{name;__channel;__messageQueue=new a;async receive(){return this.__messageQueue.pop()}tryReceive(){return this.__messageQueue.tryPop()}send(t,e){this.__channel.send(t,e)}close(){this.__channel.unsubscribe(this.__messageQueue.push)}constructor(t){this.name=t.name,this.__channel=t,this.__channel.subscribe(this.__messageQueue.push)}}class c{__alive=!0;__link;__parent;__channels=new Map;__pluginMap=new Map;__plugins=[];__negotiateChannel(t){const{port1:e,port2:n}=new MessageChannel,r=new s(t,e);this.__link.postMessage([t,n],[n]),this.__channels.set(t,r)}__verifyAlive(){if(!this.__alive)throw new e("Conduit already terminated")}registerPlugin(t,...n){this.__verifyAlive();const r=[];for(const e of t.channelAttach)this.__channels.has(e)||this.__negotiateChannel(e),r.push(this.__channels.get(e));const s=new t(this,r,...n);if(void 0!==s.name){if(this.__pluginMap.has(s.name))throw new e(`Plugin ${s.name} already registered`);this.__pluginMap.set(s.name,s)}return this.__plugins.push(s),s}unregisterPlugin(t){this.__verifyAlive();let e=0;for(let n=0;n=n;--t)delete this.__plugins[t];t.name&&this.__pluginMap.delete(t.name),t.destroy?.()}lookupPlugin(t){if(this.__verifyAlive(),!this.__pluginMap.has(t))throw new e(`Plugin ${t} not registered`);return this.__pluginMap.get(t)}terminate(){this.__verifyAlive();for(const t of this.__plugins)t.destroy?.();this.__link.terminate?.(),this.__alive=!1}__handlePort(t){const[e,n]=t;if(this.__channels.has(e)){const t=this.__channels.get(e);this.__parent?t.listenToPort(n):t.replacePort(n)}else{const t=new s(e,n);this.__channels.set(e,t)}}constructor(t,e=!1){this.__link=t,t.addEventListener("message",(t=>this.__handlePort(t.data))),this.__parent=e}}class u{type=0;data;constructor(t,e,n){this.data={fn:t,args:e,invokeId:n}}}class h{type=2;data;constructor(t,e){this.data={invokeId:t,err:e}}}class l{type=1;data;constructor(t,e){this.data={invokeId:t,res:e}}}function p(t){}var f;!function(t){t[t.VOID=0]="VOID",t[t.BOOLEAN=1]="BOOLEAN",t[t.NUMBER=2]="NUMBER",t[t.CONST_STRING=3]="CONST_STRING",t[t.EMPTY_LIST=4]="EMPTY_LIST",t[t.PAIR=5]="PAIR",t[t.ARRAY=6]="ARRAY",t[t.CLOSURE=7]="CLOSURE",t[t.OPAQUE=8]="OPAQUE",t[t.LIST=9]="LIST"}(f||(f={}));class w{type=1;data;constructor(t){this.data={minVersion:t}}}class y{type=0;data={version:0}}class d{type=3;data;constructor(t){this.data=t}}let m=(()=>{let t,n,s=[p],i=[];return class{static{n=this}static{const e="function"==typeof Symbol&&Symbol.metadata?Object.create(null):void 0;!function(t,e,n,r,s,i){function a(t){if(void 0!==t&&"function"!=typeof t)throw new TypeError("Function expected");return t}for(var o,c=r.kind,u="getter"===c?"get":"setter"===c?"set":"value",h=!e&&t?r.static?t:t.prototype:null,l=e||(h?Object.getOwnPropertyDescriptor(h,r.name):{}),p=!1,f=n.length-1;f>=0;f--){var w={};for(var y in r)w[y]="access"===y?{}:r[y];for(var y in r.access)w.access[y]=r.access[y];w.addInitializer=function(t){if(p)throw new TypeError("Cannot add initializers after decoration has completed");i.push(a(t||null))};var d=(0,n[f])("accessor"===c?{get:l.get,set:l.set}:l[u],w);if("accessor"===c){if(void 0===d)continue;if(null===d||"object"!=typeof d)throw new TypeError("Object expected");(o=a(d.get))&&(l.get=o),(o=a(d.set))&&(l.set=o),(o=a(d.init))&&s.unshift(o)}else(o=a(d))&&("field"===c?s.unshift(o):l[u]=o)}h&&Object.defineProperty(h,r.name,l),p=!0}(null,t={value:n},s,{kind:"class",name:n.name,metadata:e},null,i),n=t.value,e&&Object.defineProperty(n,Symbol.metadata,{enumerable:!0,configurable:!0,writable:!0,value:e})}name="__runner_main";__evaluator;__isCompatibleWithModules;__conduit;__fileRpc;__chunkQueue;__serviceChannel;__ioQueue;__errorChannel;__statusChannel;__serviceHandlers=new Map([[0,function(t){t.data.version<0?(this.__serviceChannel.send(new w(0)),console.error(`Host's protocol version (${t.data.version}) must be at least 0`)):console.log(`Host is using protocol version ${t.data.version}`)}],[1,function(t){console.error(`Host expects at least protocol version ${t.data.minVersion}, but we are on version 0`),this.__conduit.terminate()}],[2,function(t){this.__evaluator.startEvaluator(t.data)}]]);requestFile(t){return this.__fileRpc.requestFile(t)}async requestChunk(){return(await this.__chunkQueue.receive()).chunk}async requestInput(){const{message:t}=await this.__ioQueue.receive();return t}tryRequestInput(){const t=this.__ioQueue.tryReceive();return t?.message}sendOutput(t){this.__ioQueue.send({message:t})}sendError(t){this.__errorChannel.send({error:t})}updateStatus(t,e){this.__statusChannel.send({status:t,isActive:e})}hostLoadPlugin(t){this.__serviceChannel.send(new d(t))}registerPlugin(t,...e){return this.__conduit.registerPlugin(t,...e)}unregisterPlugin(t){this.__conduit.unregisterPlugin(t)}registerModule(t){if(!this.__isCompatibleWithModules)throw new e("Evaluator has no data interface");return this.registerPlugin(t,this.__evaluator)}unregisterModule(t){this.unregisterPlugin(t)}async importAndRegisterExternalPlugin(t){const e=await r(t);return this.registerPlugin(e)}async importAndRegisterExternalModule(t){const e=await async function(t){return await r(t)}(t);return this.registerModule(e)}static channelAttach=["__file_rpc","__chunk","__service","__stdio","__error","__status"];constructor(t,[e,n,r,s,i,a],c){this.__conduit=t,this.__fileRpc=function(t,e){const n=[];let r=0;return t.subscribe((async r=>{switch(r.type){case 0:{const{fn:n,args:s,invokeId:i}=r.data;try{const r=await e[n](...s);i>0&&t.send(new l(i,r))}catch(e){i>0&&t.send(new h(i,e))}break}case 1:{const{invokeId:t,res:e}=r.data;n[t]?.[0]?.(e),delete n[t];break}case 2:{const{invokeId:t,err:e}=r.data;n[t]?.[1]?.(e),delete n[t];break}}})),new Proxy({},{get(e,s,i){const a=Reflect.get(e,s,i);if(a)return a;const o="string"==typeof s&&"$"===s.charAt(0)?(...e)=>{t.send(new u(s,e,0))}:(...e)=>{const i=++r;return t.send(new u(s,e,i)),new Promise(((t,e)=>{n[i]=[t,e]}))};return Reflect.set(e,s,o,i),o}})}(e,{}),this.__chunkQueue=new o(n),this.__serviceChannel=r,this.__ioQueue=new o(s),this.__errorChannel=i,this.__statusChannel=a,this.__serviceChannel.send(new y),this.__serviceChannel.subscribe((t=>{this.__serviceHandlers.get(t.type)?.call(this,t)})),this.__evaluator=new c(this),this.__isCompatibleWithModules=this.__evaluator.hasDataInterface??!1}static{!function(t,e,n){for(var r=arguments.length>2,s=0;st===e))){return P(t,function(t){const[e,n]=b(t,t.length-1);return[e,n]}(e))}return e}function P(t,e){const n=function([t,e]){const n=function(t){const e=t.toString().split("").map((t=>g[t]||t)).join("");return e}(e);return t+n}(e);return t.map((t=>t.toString())).includes(n.toString())?P(t,function(t){return[t[0],t[1]+1]}(e)):n}function T(t){const e=t.split("").map((t=>v[t]||t)).join("");return parseInt(e,10)||1}function b(t,e){return e<0?[t,0]:(n=t[e],Object.keys(v).includes(n)?b(t,e-1):[t.substring(0,e+1),T(t.substring(e+1))]);var n}class N{location;varName;constructor(t,e){this.location=t,this.varName=e}}class x{binder;type;constructor(t,e){this.binder=t,this.type=e}}class _{message;constructor(t){this.message=t}}class k{}class S extends k{result;constructor(t){super(),this.result=t}}class $ extends k{where;message;constructor(t,e){super(),this.where=t,this.message=e}}class O{name;value;constructor(t,e=null){this.name=t,this.value=e}}function L(t,e){for(const[e,n]of t){const r=n();if(!(r instanceof S))throw new Error(`Encountered stop when evaluating the sequence ${t}. Error message: ${r.message.message} at ${r.where}`);e.value=r.result}return e()}class A{constructor(){}}class I extends A{env;varName;expr;constructor(t,e,n){super(),this.env=t,this.varName=e,this.expr=n}valOfClosure(t){return this.expr.valOf((e=this.env,n=this.varName,r=t,new Map([...e,[n,r]])));var e,n,r}prettyPrint(){return`(CLOS ${this.varName} ${this.expr.prettyPrint()})`}toString(){return this.prettyPrint()}}class B extends A{proc;constructor(t){super(),this.proc=t}valOfClosure(t){return this.proc(t)}prettyPrint(){return"(HOCLOS)"}toString(){return this.prettyPrint()}}function C(t){return!("U"===(e=t)||"Nat"===e||"zero"===e||"add1"===e||"which-Nat"===e||"iter-Nat"===e||"rec-Nat"===e||"ind-Nat"===e||"->"===e||"→"===e||"Π"===e||"λ"===e||"Pi"===e||"∏"===e||"lambda"===e||"quote"===e||"Atom"===e||"car"===e||"cdr"===e||"cons"===e||"Σ"===e||"Sigma"===e||"Pair"===e||"Trivial"===e||"sole"===e||"List"===e||"::"===e||"nil"===e||"rec-List"===e||"ind-List"===e||"Absurd"===e||"ind-Absurd"===e||"="===e||"same"===e||"replace"===e||"trans"===e||"cong"===e||"symm"===e||"ind-="===e||"Vec"===e||"vecnil"===e||"vec::"===e||"head"===e||"tail"===e||"ind-Vec"===e||"Either"===e||"left"===e||"right"===e||"ind-Either"===e||"TODO"===e||"the"===e)&&isNaN(Number(t));var e}function R(t){return Array.from(t.keys())}function q(t,e){return E(R(t),e)}function M(t,e,n){return E(R(t).concat(e.findNames()),n)}function U(t){return[t.binder.varName].concat(t.type.findNames())}function H(t,e,n){return new Map([...t,[e,n]])}function D(t,e){return e.valOf(V(t))}function z(t){const e=new Map;for(const[n,r]of t)r instanceof Z?e.set(n,["free",r.type.readBackType(t)]):r instanceof Y?e.set(n,["def",r.type.readBackType(t),lt(t,r.type,r.value)]):r instanceof K&&e.set(n,["claim",r.type.readBackType(t)]);return e}function Q(t,e,n,r){const s=new O("typeOut");return L([[new O("_"),()=>function(t,e,n){return t.has(n)?new $(e,new _([`The name "${n}" is already in use in the context.`])):new S(!0)}(t,n,e)],[s,()=>r.isType(t,new Map)]],(()=>new S(H(t,e,new K(D(t,s.value))))))}function F(t,e,n,r){const s=new O("typeOut"),i=new O("exprOut");return L([[s,()=>function(t,e,n){for(const[r,s]of t)if(r===n){if(s instanceof Y)return new $(e,new _([`The name "${n}" is already defined.`]));if(s instanceof K)return new S(s.type)}return new $(e,new _([`No claim: ${n}`]))}(t,n,e)],[i,()=>r.check(t,new Map,s.value)]],(()=>new S(function(t,e,n,r){return H(t,e,new Y(n,r))}(function(t,e){return t.delete(e),t}(t,e),e,s.value,D(t,i.value)))))}function V(t){if(0===t.size)return new Map;const e=t.entries(),n=new Map;for(const[t,r]of e)r instanceof Y?n.set(t,r.value):r instanceof Z&&n.set(t,new oe(r.type,new wt(t)));return n}const G=new Map;class X{}let K=class extends X{type;constructor(t){super(),this.type=t}};class Y extends X{type;value;constructor(t,e){super(),this.type=t,this.value=e}}class Z extends X{type;constructor(t){super(),this.type=t}}function j(t,e,n){if(0===t.size)throw new Error(`Unknown variable ${n}`);for(const[e,r]of t.entries())if(!(r instanceof K)&&n===e)return new S(r.type);throw new Error(`Unknown variable ${n}`)}function W(t,e,n){if(t.has(e)){for(const[r,s]of t)if(r===e)return H(t,e,new Z(n));throw new Error(`\n ${e} is already bound in ${JSON.stringify(t)}\n `)}return H(t,e,new Z(n))}function J(t,e){const n=t.now();if(n instanceof Xt)return n.body.valOfClosure(e);if(n instanceof oe){const t=n.type.now();if(t instanceof Gt)return new oe(t.resultType.valOfClosure(e),new qt(n.neutral,new pt(t.argType,e)))}throw new Error(`doApp: invalid input ${[n,e]}`)}function tt(t,e,n,r){const s=t.now();if(s instanceof Ft)return n;if(s instanceof Vt)return J(r,tt(s.smaller,e,n,r));if(s instanceof oe){if(s.type.now()instanceof Qt)return new oe(e,new mt(s.neutral,new pt(e,n),new pt(new Gt("n",new Qt,new B((t=>e))),r)))}throw new Error(`invalid input for iterNat ${[t,e,n,r]}`)}function et(t,e,n,r){const s=t.now();if(s instanceof Ft)return n;if(s instanceof Vt)return J(J(r,s.smaller),et(s.smaller,e,n,r));if(s instanceof oe){if(s.type.now()instanceof Qt)return new oe(e,new gt(s.neutral,new pt(e,n),new pt(new Gt("n-1",new Qt,new B((t=>new Gt("ih",e,new B((t=>e)))))),r)))}throw new Error(`invalid input for recNat ${[t,e,n,r]}`)}function nt(t,e,n,r){const s=t.now();if(s instanceof Ft)return n;if(s instanceof Vt)return J(J(r,s.smaller),nt(s.smaller,e,n,r));if(s instanceof oe){if(s.type.now()instanceof Qt)return new oe(J(e,t),new vt(s.neutral,new pt(new Gt("x",new Qt,new B((t=>new ce))),e),new pt(J(e,new Ft),n),new pt(new Gt("n-1",new Qt,new B((t=>new Gt("ih",J(e,t),new B((n=>J(e,new Vt(t)))))))),r)))}throw new Error(`invalid input for indNat ${[t,e,n,r]}`)}function rt(t){const e=t.now();if(e instanceof Yt)return e.car;if(e instanceof oe){const t=e.type.now();if(t instanceof Kt){const n=t,r=e.neutral;return new oe(n.carType,new Et(r))}}throw new Error(`invalid input for car ${t}`)}function st(t){const e=t.now();if(e instanceof Yt)return e.cdr;if(e instanceof oe){const n=e.type.now();if(n instanceof Kt){const r=n,s=e.neutral;return new oe(r.cdrType.valOfClosure(rt(t)),new Pt(s))}}throw new Error(`invalid input for cdr ${t}`)}function it(t,e,n,r){const s=t.now();if(s instanceof jt)return n;if(s instanceof Wt)return J(J(J(r,s.head),s.tail),it(s.tail,e,n,r));if(s instanceof oe){const i=s.type.now();if(i instanceof Zt){const a=i.entryType,o=s.neutral,c=new Gt("xs",new Zt(a),new B((t=>new ce)));return new oe(J(e,t),new bt(o,new pt(c,e),new pt(J(e,new jt),n),new pt(new Gt("h",a,new B((t=>new Gt("t",new Zt(a),new B((n=>new Gt("ih",J(e,n),new B((r=>J(e,new Wt(t,n))))))))))),r)))}}throw new Error(`invalid input for indList ${[s,e,n,r]}`)}function at(t,e,n,r){const s=t.now();if(s instanceof jt)return n;if(s instanceof Wt){const t=s.head,i=s.tail;return J(J(J(r,t),i),at(i,e,n,r))}if(s instanceof oe){const t=s.type.now();if(t instanceof Zt){const i=t.entryType,a=s.neutral;return new oe(e,new Tt(a,new pt(e,n),new pt(new Gt("h",i,new B((t=>new Gt("t",new Zt(i),new B((t=>new Gt("ih",e,new B((t=>e))))))))),r)))}}throw new Error(`invalid input for recList ${[s,e,n,r]}`)}function ot(t){const e=t.now();if(e instanceof re)return e.tail;if(e instanceof oe&&e.type instanceof ee&&e.type.length instanceof Vt){const t=e.type.now();if(t instanceof ee){if(t.length.now()instanceof Vt)return new oe(new ee(e.type.entryType,e.type.length.smaller),new It(e.neutral))}}throw new Error(`invalid input for tail ${t}`)}function ct(t,e){return new Gt("k",new Qt,new B((n=>new Gt("e",new ee(t,n),new B((r=>new Gt("es",new ee(t,n),new B((t=>new Gt("ih",J(J(e,n),t),new B((s=>J(J(e,new Vt(n)),new re(r,t))))))))))))))}function ut(t,e,n,r,s){const i=t.now(),a=e.now();if(i instanceof Ft&&a instanceof ne)return r;if(i instanceof Vt&&a instanceof re)return J(J(J(J(s,i.smaller),a.head),ot(e)),ut(i.smaller,a.tail,n,r,s));if(i instanceof oe&&a instanceof oe&&i.type instanceof Qt&&a.type instanceof ee){const o=a.type.entryType;return new oe(J(J(n,t),e),new Ct(i.neutral,a.neutral,new pt(new Gt("k",new Qt,new B((t=>new Gt("es",new ee(o,t),new B((t=>new ce)))))),n),new pt(J(J(n,new Ft),new ne),r),new pt(ct(a.type.entryType,n),s)))}if(ht(i,t)&&a instanceof oe&&a.type instanceof ee){const i=a.type.entryType;return new oe(J(J(n,t),e),new Bt(new pt(new Qt,t),a.neutral,new pt(new Gt("k",new Qt,new B((t=>new Gt("es",new ee(i,t),new B((t=>new ce)))))),n),new pt(J(J(n,new Qt),new ne),r),new pt(ct(i,n),s)))}throw new Error(`invalid input for indVec ${[t,e,n,r,s]}`)}function ht(t,e){const n=t.now(),r=e.now();return n instanceof Ft&&r instanceof Ft||n instanceof Vt&&r instanceof Vt&&ht(n.smaller,r.smaller)}function lt(t,e,n){const r=e.now(),s=n.now();if(r instanceof ce)return n.readBackType(t);if(r instanceof Qt&&s instanceof Ft)return new me;if(r instanceof Qt&&s instanceof Vt)return new ge(lt(t,new Qt,s.smaller));if(r instanceof Gt){const e=q(t,s instanceof Xt?s.argName:r.argName);return new Ne(e,lt(W(t,e,r.argType),r.resultType.valOfClosure(new oe(r.argType,new wt(e))),J(s,new oe(r.argType,new wt(e)))))}if(r instanceof Kt){const e=rt(n),s=st(n);return new Se(lt(t,r.carType,e),lt(t,r.cdrType.valOfClosure(e),s))}if(r instanceof ue&&s instanceof zt)return new _e(s.name);if(r instanceof he)return new qe;if(r instanceof Zt&&s instanceof jt)return new Ae;if(r instanceof Zt&&s instanceof Wt)return new Se(lt(t,r.entryType,s.head),lt(t,new Zt(r.entryType),s.tail));if(r instanceof pe&&s instanceof oe)return new we(new Me,s.neutral.readBackNeutral(t));if(r instanceof Jt&&s instanceof te)return new De(lt(t,r.type,s.value));if(r instanceof ee&&r.length.now()instanceof Ft)return new Ye;if(r instanceof ee&&r.length.now()instanceof Vt&&s instanceof re){const e=r.length.now();return new Ke(lt(t,r.entryType,s.head),lt(t,new ee(r.entryType,e.smaller),s.tail))}if(r instanceof se&&s instanceof ie)return new tn(lt(t,r.leftType,s.value));if(r instanceof se&&s instanceof ae)return new en(lt(t,r.rightType,s.value));if(s instanceof oe)return s.neutral.readBackNeutral(t);throw new Error(`Cannot read back ${s} : ${r}`)}class pt{type;value;constructor(t,e){this.type=t,this.value=e}}let ft=class{constructor(){}toString(){return this.prettyPrint()}};class wt extends ft{name;constructor(t){super(),this.name=t}readBackNeutral(t){return new an(this.name)}prettyPrint(){return`N-${this.name}`}}let yt=class extends ft{where;type;constructor(t,e){super(),this.where=t,this.type=e}readBackNeutral(t){return new rn(this.where,this.type.readBackType(t))}prettyPrint(){return"N-TODO"}},dt=class extends ft{target;base;step;constructor(t,e,n){super(),this.target=t,this.base=e,this.step=n}readBackNeutral(t){return new ve(this.target.readBackNeutral(t),new we(this.base.type.readBackType(t),lt(t,this.base.type,this.base.value)),lt(t,this.step.type,this.step.value))}prettyPrint(){return"N-WhichNat"}},mt=class extends ft{target;base;step;constructor(t,e,n){super(),this.target=t,this.base=e,this.step=n}readBackNeutral(t){return new Ee(this.target.readBackNeutral(t),new we(this.base.type.readBackType(t),lt(t,this.base.type,this.base.value)),lt(t,this.step.type,this.step.value))}prettyPrint(){return"N-IterNat"}},gt=class extends ft{target;base;step;constructor(t,e,n){super(),this.target=t,this.base=e,this.step=n}readBackNeutral(t){return new Pe(this.target.readBackNeutral(t),new we(this.base.type.readBackType(t),lt(t,this.base.type,this.base.value)),lt(t,this.step.type,this.step.value))}prettyPrint(){return"N-RecNat"}},vt=class extends ft{target;motive;base;step;constructor(t,e,n,r){super(),this.target=t,this.motive=e,this.base=n,this.step=r}readBackNeutral(t){return new Te(this.target.readBackNeutral(t),lt(t,this.motive.type,this.motive.value),lt(t,this.base.type,this.base.value),lt(t,this.step.type,this.step.value))}prettyPrint(){return"N-IndNat"}},Et=class extends ft{target;constructor(t){super(),this.target=t}readBackNeutral(t){return new $e(this.target.readBackNeutral(t))}prettyPrint(){return"N-Car"}},Pt=class extends ft{target;constructor(t){super(),this.target=t}readBackNeutral(t){return new Oe(this.target.readBackNeutral(t))}prettyPrint(){return"N-Cdr"}},Tt=class extends ft{target;base;step;constructor(t,e,n){super(),this.target=t,this.base=e,this.step=n}readBackNeutral(t){return new Be(this.target.readBackNeutral(t),new we(this.base.type.readBackType(t),lt(t,this.base.type,this.base.value)),lt(t,this.step.type,this.step.value))}prettyPrint(){return"N-RecList"}},bt=class extends ft{target;motive;base;step;constructor(t,e,n,r){super(),this.target=t,this.motive=e,this.base=n,this.step=r}readBackNeutral(t){return new Ce(this.target.readBackNeutral(t),lt(t,this.motive.type,this.motive.value),lt(t,this.base.type,this.base.value),lt(t,this.step.type,this.step.value))}prettyPrint(){return"N-IndList"}},Nt=class extends ft{target;motive;constructor(t,e){super(),this.target=t,this.motive=e}readBackNeutral(t){return new Ue(new we(new Me,this.target.readBackNeutral(t)),lt(t,this.motive.type,this.motive.value))}prettyPrint(){return"N-IndAbsurd"}},xt=class extends ft{target;motive;base;constructor(t,e,n){super(),this.target=t,this.motive=e,this.base=n}readBackNeutral(t){return new ze(this.target.readBackNeutral(t),lt(t,this.motive.type,this.motive.value),lt(t,this.base.type,this.base.value))}prettyPrint(){return"N-Replace"}};class _t extends ft{target1;target2;constructor(t,e){super(),this.target1=t,this.target2=e}readBackNeutral(t){return new Qe(this.target1.readBackNeutral(t),lt(t,this.target2.type,this.target2.value))}prettyPrint(){return"N-Trans1"}}class kt extends ft{target1;target2;constructor(t,e){super(),this.target1=t,this.target2=e}readBackNeutral(t){return new Qe(lt(t,this.target1.type,this.target1.value),this.target2.readBackNeutral(t))}prettyPrint(){return"N-Trans2"}}class St extends ft{target1;target2;constructor(t,e){super(),this.target1=t,this.target2=e}readBackNeutral(t){return new Qe(this.target1.readBackNeutral(t),this.target2.readBackNeutral(t))}prettyPrint(){return"N-Trans12"}}let $t=class extends ft{target;func;constructor(t,e){super(),this.target=t,this.func=e}readBackNeutral(t){const e=this.func.type;if(e instanceof Gt){const n=e.resultType;return new Fe(this.target.readBackNeutral(t),n.valOfClosure(new pe).readBackType(t),lt(t,this.func.type,this.func.value))}throw new Error("Cong applied to non-Pi type.")}prettyPrint(){return"N-Cong"}},Ot=class extends ft{target;constructor(t){super(),this.target=t}readBackNeutral(t){return new Ve(this.target.readBackNeutral(t))}prettyPrint(){return"N-Symm"}},Lt=class extends ft{target;motive;base;constructor(t,e,n){super(),this.target=t,this.motive=e,this.base=n}readBackNeutral(t){return new Ge(this.target.readBackNeutral(t),lt(t,this.motive.type,this.motive.value),lt(t,this.base.type,this.base.value))}prettyPrint(){return"N-IndEqual"}},At=class extends ft{target;constructor(t){super(),this.target=t}readBackNeutral(t){return new Ze(this.target.readBackNeutral(t))}prettyPrint(){return"N-Head"}},It=class extends ft{target;constructor(t){super(),this.target=t}readBackNeutral(t){return new je(this.target.readBackNeutral(t))}prettyPrint(){return"N-Tail"}};class Bt extends ft{length;target;motive;base;step;constructor(t,e,n,r,s){super(),this.length=t,this.target=e,this.motive=n,this.base=r,this.step=s}readBackNeutral(t){return new We(lt(t,this.length.type,this.length.value),this.target.readBackNeutral(t),lt(t,this.motive.type,this.motive.value),lt(t,this.base.type,this.base.value),lt(t,this.step.type,this.step.value))}prettyPrint(){return"N-IndVec2"}}class Ct extends ft{length;target;motive;base;step;constructor(t,e,n,r,s){super(),this.length=t,this.target=e,this.motive=n,this.base=r,this.step=s}readBackNeutral(t){return new We(this.length.readBackNeutral(t),this.target.readBackNeutral(t),lt(t,this.motive.type,this.motive.value),lt(t,this.base.type,this.base.value),lt(t,this.step.type,this.step.value))}prettyPrint(){return"N-IndVec12"}}let Rt=class extends ft{target;motive;baseLeft;baseRight;constructor(t,e,n,r){super(),this.target=t,this.motive=e,this.baseLeft=n,this.baseRight=r}readBackNeutral(t){return new nn(this.target.readBackNeutral(t),lt(t,this.motive.type,this.motive.value),lt(t,this.baseLeft.type,this.baseLeft.value),lt(t,this.baseRight.type,this.baseRight.value))}prettyPrint(){return"N-IndEither"}},qt=class extends ft{operator;operand;constructor(t,e){super(),this.operator=t,this.operand=e}readBackNeutral(t){return new sn(this.operator.readBackNeutral(t),lt(t,this.operand.type,this.operand.value))}prettyPrint(){return"N-Application"}};class Mt{now(){return this}}class Ut{env;expr;constructor(t,e){this.env=t,this.expr=e}undelay(){return this.expr.valOf(this.env).now()}toString(){return`DelayClosure(${this.env}, ${this.expr})`}}class Ht{content;constructor(t){this.content=t}get(){return this.content}set(t){this.content=t}}class Dt extends Mt{val;constructor(t){super(),this.val=t}now(){const t=this.val.get();if(t instanceof Ut){let e=t.undelay();return this.val.set(e),e}return t}readBackType(t){return this.now().readBackType(t)}prettyPrint(){return this.now().prettyPrint()}toString(){return`Delay(${this.val})`}}let zt=class extends Mt{name;constructor(t){super(),this.name=t}readBackType(t){throw new Error("No readBackType for Quote.")}prettyPrint(){return`'${this.name}`}toString(){return this.prettyPrint()}},Qt=class extends Mt{constructor(){super()}readBackType(t){return new de}prettyPrint(){return"Nat"}toString(){return this.prettyPrint()}},Ft=class extends Mt{constructor(){super()}readBackType(t){throw new Error("No readBackType for Zero.")}prettyPrint(){return"zero"}toString(){return this.prettyPrint()}},Vt=class extends Mt{smaller;constructor(t){super(),this.smaller=t}readBackType(t){throw new Error("No readBackType for Add1.")}prettyPrint(){return`(add1 ${this.smaller.prettyPrint()})`}toString(){return this.prettyPrint()}},Gt=class extends Mt{argName;argType;resultType;constructor(t,e,n){super(),this.argName=t,this.argType=e,this.resultType=n}readBackType(t){const e=this.argType.readBackType(t),n=q(t,this.argName),r=W(t,n,this.argType);return new be(n,e,this.resultType.valOfClosure(new oe(this.argType,new wt(n))).readBackType(r))}prettyPrint(){return`(Π ${this.argName} ${this.argType.prettyPrint()} ${this.resultType.prettyPrint()})`}toString(){return this.prettyPrint()}},Xt=class extends Mt{argName;body;constructor(t,e){super(),this.argName=t,this.body=e}readBackType(t){throw new Error("No readBackType for Lambda.")}prettyPrint(){return`(lambda ${this.argName} ${this.body.prettyPrint()})`}toString(){return this.prettyPrint()}},Kt=class extends Mt{carName;carType;cdrType;constructor(t,e,n){super(),this.carName=t,this.carType=e,this.cdrType=n}readBackType(t){const e=this.carType.readBackType(t),n=q(t,this.carName),r=W(t,n,this.carType);return new ke(n,e,this.cdrType.valOfClosure(new oe(this.carType,new wt(n))).readBackType(r))}prettyPrint(){return`(Σ ${this.carName} ${this.carType.prettyPrint()} ${this.cdrType.prettyPrint()})`}toString(){return this.prettyPrint()}},Yt=class extends Mt{car;cdr;constructor(t,e){super(),this.car=t,this.cdr=e}readBackType(t){throw new Error("No readBackType for Cons.")}prettyPrint(){return`(cons ${this.car.prettyPrint()} ${this.cdr.prettyPrint()})`}toString(){return this.prettyPrint()}},Zt=class extends Mt{entryType;constructor(t){super(),this.entryType=t}readBackType(t){return new Ie(this.entryType.readBackType(t))}prettyPrint(){return`(List ${this.entryType.prettyPrint()})`}toString(){return this.prettyPrint()}},jt=class extends Mt{constructor(){super()}readBackType(t){throw new Error("No readBackType for Nil.")}prettyPrint(){return"nil"}toString(){return this.prettyPrint()}},Wt=class extends Mt{head;tail;constructor(t,e){super(),this.head=t,this.tail=e}readBackType(t){throw new Error("No readBackType for ListCons.")}prettyPrint(){return`(:: ${this.head.prettyPrint()} ${this.tail.prettyPrint()})`}toString(){return this.prettyPrint()}},Jt=class extends Mt{type;from;to;constructor(t,e,n){super(),this.type=t,this.from=e,this.to=n}readBackType(t){return new He(this.type.readBackType(t),lt(t,this.type,this.from),lt(t,this.type,this.to))}prettyPrint(){return`(= ${this.type.prettyPrint()} ${this.from.prettyPrint()} ${this.to.prettyPrint()})`}toString(){return this.prettyPrint()}},te=class extends Mt{value;constructor(t){super(),this.value=t}readBackType(t){throw new Error("No readBackType for Same.")}prettyPrint(){return`(same ${this.value.prettyPrint()})`}toString(){return this.prettyPrint()}},ee=class extends Mt{entryType;length;constructor(t,e){super(),this.entryType=t,this.length=e}readBackType(t){return new Xe(this.entryType.readBackType(t),lt(t,new Qt,this.length))}prettyPrint(){return`(Vec ${this.entryType.prettyPrint()} ${this.length.prettyPrint()})`}},ne=class extends Mt{constructor(){super()}readBackType(t){throw new Error("No readBackType for VecNil.")}prettyPrint(){return"vecnil"}toString(){return this.prettyPrint()}},re=class extends Mt{head;tail;constructor(t,e){super(),this.head=t,this.tail=e}readBackType(t){throw new Error("No readBackType for VecCons.")}prettyPrint(){return`(vec:: ${this.head.prettyPrint()} ${this.tail.prettyPrint()})`}toString(){return this.prettyPrint()}},se=class extends Mt{leftType;rightType;constructor(t,e){super(),this.leftType=t,this.rightType=e}readBackType(t){return new Je(this.leftType.readBackType(t),this.rightType.readBackType(t))}prettyPrint(){return`(Either ${this.leftType.prettyPrint()} ${this.rightType.prettyPrint()})`}toString(){return this.prettyPrint()}},ie=class extends Mt{value;constructor(t){super(),this.value=t}readBackType(t){throw new Error("No readBackType for Left.")}prettyPrint(){return`(left ${this.value.prettyPrint()})`}toString(){return this.prettyPrint()}},ae=class extends Mt{value;constructor(t){super(),this.value=t}readBackType(t){throw new Error("No readBackType for Right.")}prettyPrint(){return`(right ${this.value.prettyPrint()})`}toString(){return this.prettyPrint()}};class oe extends Mt{type;neutral;constructor(t,e){super(),this.type=t,this.neutral=e}readBackType(t){return this.neutral.readBackNeutral(t)}prettyPrint(){return`(Neutral ${this.type.prettyPrint()} ${this.neutral.prettyPrint()})`}toString(){return this.prettyPrint()}}let ce=class extends Mt{constructor(){super()}readBackType(t){return new ye}prettyPrint(){return"U"}toString(){return this.prettyPrint()}},ue=class extends Mt{constructor(){super()}readBackType(t){return new xe}prettyPrint(){return"Atom"}toString(){return this.prettyPrint()}},he=class extends Mt{constructor(){super()}readBackType(t){return new Re}prettyPrint(){return"Trivial"}toString(){return this.prettyPrint()}},le=class extends Mt{constructor(){super()}readBackType(t){throw new Error("No readBackType for Sole.")}prettyPrint(){return"sole"}toString(){return this.prettyPrint()}},pe=class extends Mt{constructor(){super()}readBackType(t){return new Me}prettyPrint(){return"Absurd"}toString(){return this.prettyPrint()}};class fe{toLazy(t){return new Dt(new Ht(new Ut(t,this)))}}let we=class extends fe{type;expr;constructor(t,e){super(),this.type=t,this.expr=e}valOf(t){return this.expr.valOf(t)}prettyPrint(){return`(the ${this.type.prettyPrint()} ${this.expr.prettyPrint()})`}toString(){return this.prettyPrint()}},ye=class extends fe{valOf(t){return new ce}prettyPrint(){return"U"}toString(){return this.prettyPrint()}},de=class extends fe{valOf(t){return new Qt}prettyPrint(){return"Nat"}toString(){return this.prettyPrint()}},me=class extends fe{valOf(t){return new Ft}prettyPrint(){return"0"}toString(){return this.prettyPrint()}},ge=class extends fe{n;constructor(t){super(),this.n=t}valOf(t){return new Vt(this.n.toLazy(t))}prettyPrint(){return isNaN(Number(this.n.prettyPrint()))?`(add1 ${this.n.prettyPrint()})`:`${Number(this.n.prettyPrint())+1}`}toString(){return this.prettyPrint()}},ve=class extends fe{target;base;step;constructor(t,e,n){super(),this.target=t,this.base=e,this.step=n}valOf(t){return function(t,e,n,r){const s=t.now();if(s instanceof Ft)return n;if(s instanceof Vt)return J(r,s.smaller);if(s instanceof oe&&s.type.now()instanceof Qt)return new oe(e,new dt(s.neutral,new pt(e,n),new pt(new Gt("n",new Qt,new B((t=>e))),r)));throw new Error(`invalid input for whichNat ${[t,e,n,r]}`)}(this.target.toLazy(t),this.base.type.toLazy(t),this.base.expr.toLazy(t),this.step.toLazy(t))}prettyPrint(){return`(which-Nat ${this.target.prettyPrint()} \n ${this.base.prettyPrint()} \n ${this.step.prettyPrint()})`}toString(){return this.prettyPrint()}},Ee=class extends fe{target;base;step;constructor(t,e,n){super(),this.target=t,this.base=e,this.step=n}valOf(t){return tt(this.target.toLazy(t),this.base.type.toLazy(t),this.base.expr.toLazy(t),this.step.toLazy(t))}prettyPrint(){return`(iter-Nat ${this.target.prettyPrint()} \n ${this.base.prettyPrint()} \n ${this.step.prettyPrint()})`}toString(){return this.prettyPrint()}},Pe=class extends fe{target;base;step;constructor(t,e,n){super(),this.target=t,this.base=e,this.step=n}valOf(t){return et(this.target.toLazy(t),this.base.type.toLazy(t),this.base.expr.toLazy(t),this.step.toLazy(t))}prettyPrint(){return`(rec-Nat ${this.target.prettyPrint()} \n ${this.base.prettyPrint()} \n ${this.step.prettyPrint()})`}toString(){return this.prettyPrint()}},Te=class extends fe{target;motive;base;step;constructor(t,e,n,r){super(),this.target=t,this.motive=e,this.base=n,this.step=r}valOf(t){return nt(this.target.toLazy(t),this.motive.toLazy(t),this.base.toLazy(t),this.step.toLazy(t))}prettyPrint(){return`(ind-Nat ${this.target.prettyPrint()} \n ${this.motive.prettyPrint()} \n ${this.base.prettyPrint()} \n ${this.step.prettyPrint()})`}toString(){return this.prettyPrint()}},be=class extends fe{name;type;body;constructor(t,e,n){super(),this.name=t,this.type=e,this.body=n}valOf(t){const e=this.type.toLazy(t);return new Gt(this.name,e,new I(t,this.name,this.body))}prettyPrint(){return`(Π (${this.name} ${this.type.prettyPrint()}) \n ${this.body.prettyPrint()})`}toString(){return this.prettyPrint()}},Ne=class extends fe{param;body;constructor(t,e){super(),this.param=t,this.body=e}valOf(t){return new Xt(this.param,new I(t,this.param,this.body))}prettyPrint(){return`(λ (${this.param}) ${this.body.prettyPrint()})`}toString(){return this.prettyPrint()}},xe=class extends fe{valOf(t){return new ue}prettyPrint(){return"Atom"}toString(){return this.prettyPrint()}},_e=class extends fe{sym;constructor(t){super(),this.sym=t}valOf(t){return new zt(this.sym)}prettyPrint(){return`'${this.sym}`}toString(){return this.prettyPrint()}},ke=class extends fe{name;type;body;constructor(t,e,n){super(),this.name=t,this.type=e,this.body=n}valOf(t){const e=this.type.toLazy(t);return new Kt(this.name,e,new I(t,this.name,this.body))}prettyPrint(){return`(Σ (${this.name} ${this.type.prettyPrint()}) \n ${this.body.prettyPrint()})`}toString(){return this.prettyPrint()}},Se=class extends fe{first;second;constructor(t,e){super(),this.first=t,this.second=e}valOf(t){const e=this.first.toLazy(t),n=this.second.toLazy(t);return new Yt(e,n)}prettyPrint(){return`(cons ${this.first.prettyPrint()} ${this.second.prettyPrint()})`}toString(){return this.prettyPrint()}},$e=class extends fe{pair;constructor(t){super(),this.pair=t}valOf(t){return rt(this.pair.toLazy(t))}prettyPrint(){return`(car ${this.pair.prettyPrint()})`}toString(){return this.prettyPrint()}},Oe=class extends fe{pair;constructor(t){super(),this.pair=t}valOf(t){return st(this.pair.toLazy(t))}prettyPrint(){return`(cdr ${this.pair.prettyPrint()})`}toString(){return this.prettyPrint()}},Le=class extends fe{head;tail;constructor(t,e){super(),this.head=t,this.tail=e}valOf(t){const e=this.head.toLazy(t),n=this.tail.toLazy(t);return new Wt(e,n)}prettyPrint(){return`(:: ${this.head.prettyPrint()} ${this.tail.prettyPrint()})`}toString(){return this.prettyPrint()}},Ae=class extends fe{valOf(t){return new jt}prettyPrint(){return"nil"}toString(){return this.prettyPrint()}},Ie=class extends fe{elemType;constructor(t){super(),this.elemType=t}valOf(t){return new Zt(this.elemType.toLazy(t))}prettyPrint(){return`(List ${this.elemType.prettyPrint()})`}toString(){return this.prettyPrint()}},Be=class extends fe{target;base;step;constructor(t,e,n){super(),this.target=t,this.base=e,this.step=n}valOf(t){return at(this.target.toLazy(t),this.base.type.toLazy(t),this.base.expr.toLazy(t),this.step.toLazy(t))}prettyPrint(){return`(rec-List ${this.target.prettyPrint()} \n ${this.base.prettyPrint()} \n ${this.step.prettyPrint()})`}toString(){return this.prettyPrint()}},Ce=class extends fe{target;motive;base;step;constructor(t,e,n,r){super(),this.target=t,this.motive=e,this.base=n,this.step=r}valOf(t){return it(this.target.toLazy(t),this.motive.toLazy(t),this.base.toLazy(t),this.step.toLazy(t))}prettyPrint(){return`(ind-List ${this.target.prettyPrint()} \n ${this.motive.prettyPrint()} \n ${this.base.prettyPrint()} \n ${this.step.prettyPrint()})`}toString(){return this.prettyPrint()}},Re=class extends fe{valOf(t){return new he}prettyPrint(){return"Trivial"}toString(){return this.prettyPrint()}},qe=class extends fe{valOf(t){return new le}prettyPrint(){return"sole"}toString(){return this.prettyPrint()}},Me=class extends fe{valOf(t){return new pe}prettyPrint(){return"Absurd"}toString(){return this.prettyPrint()}},Ue=class extends fe{target;motive;constructor(t,e){super(),this.target=t,this.motive=e}valOf(t){return function(t,e){const n=t.now();if(n instanceof oe&&n.type.now()instanceof pe)return new oe(e,new Nt(n.neutral,new pt(new ce,e)));throw new Error(`invalid input for indAbsurd ${[t,e]}`)}(this.target.toLazy(t),this.motive.toLazy(t))}prettyPrint(){return`(ind-Absurd \n ${this.target.prettyPrint()} \n ${this.motive.prettyPrint()})`}toString(){return this.prettyPrint()}},He=class extends fe{type;left;right;constructor(t,e,n){super(),this.type=t,this.left=e,this.right=n}valOf(t){return new Jt(this.type.toLazy(t),this.left.toLazy(t),this.right.toLazy(t))}prettyPrint(){return`(= ${this.type.prettyPrint()} \n ${this.left.prettyPrint()} \n ${this.right.prettyPrint()})`}toString(){return this.prettyPrint()}},De=class extends fe{type;constructor(t){super(),this.type=t}valOf(t){return new te(this.type.toLazy(t))}prettyPrint(){return`(same ${this.type.prettyPrint()})`}toString(){return this.prettyPrint()}},ze=class extends fe{target;motive;base;constructor(t,e,n){super(),this.target=t,this.motive=e,this.base=n}valOf(t){return function(t,e,n){const r=t.now();if(r instanceof te)return n;if(r instanceof oe){const t=r.type.now();if(t instanceof Jt){const s=r.neutral,i=t.type,a=t.from,o=t.to;return new oe(J(e,o),new xt(s,new pt(new Gt("x",i,new B((t=>new ce))),e),new pt(J(e,a),n)))}}throw new Error(`invalid input for replace ${[t,e,n]}`)}(this.target.toLazy(t),this.motive.toLazy(t),this.base.toLazy(t))}prettyPrint(){return`(replace ${this.target.prettyPrint()} \n ${this.motive.prettyPrint()} \n ${this.base.prettyPrint()})`}toString(){return this.prettyPrint()}},Qe=class extends fe{left;right;constructor(t,e){super(),this.left=t,this.right=e}valOf(t){return function(t,e){const n=t.now(),r=e.now();if(n instanceof te&&r instanceof te)return new te(n.value);if(n instanceof te&&r instanceof oe){const t=r.type.now();if(t instanceof Jt){const e=n.value,s=t.to,i=t.type,a=r.neutral;return new oe(new Jt(i,e,s),new kt(new pt(new Jt(i,e,e),new te(e)),a))}}else if(n instanceof oe&&r instanceof te){const t=n.type.now();if(t instanceof Jt){const e=t.from,s=r.value,i=t.type,a=n.neutral;return new oe(new Jt(i,e,s),new _t(a,new pt(new Jt(i,s,s),new te(s))))}}else if(n instanceof oe&&r instanceof oe){const t=n.type.now(),e=r.type.now();if(t instanceof Jt&&e instanceof Jt){const s=t.from,i=e.to,a=t.type,o=n.neutral,c=r.neutral;return new oe(new Jt(a,s,i),new St(o,c))}}throw new Error(`invalid input for do-trans: ${[t,e]}`)}(this.left.toLazy(t),this.right.toLazy(t))}prettyPrint(){return`(trans ${this.left.prettyPrint()} ${this.right.prettyPrint()})`}toString(){return this.prettyPrint()}},Fe=class extends fe{target;base;fun;constructor(t,e,n){super(),this.target=t,this.base=e,this.fun=n}valOf(t){return function(t,e,n){const r=t.now();if(r instanceof te)return new te(J(n,r.value));if(r instanceof oe){const t=r.type.now();if(t instanceof Jt){const s=t.type,i=t.from,a=t.to,o=r.neutral;return new oe(new Jt(e,J(n,i),J(n,a)),new $t(o,new pt(new Gt("x",s,new B((t=>e))),n)))}}throw new Error(`invalid input for cong ${[t,e,n]}`)}(this.target.toLazy(t),this.base.toLazy(t),this.fun.toLazy(t))}prettyPrint(){return`(cong ${this.target.prettyPrint()} ${this.fun.prettyPrint()})`}toString(){return this.prettyPrint()}},Ve=class extends fe{equality;constructor(t){super(),this.equality=t}valOf(t){return function(t){const e=t.now();if(e instanceof te)return new te(e.value);if(e instanceof oe){const t=e.type.now();if(t instanceof Jt)return new oe(new Jt(t.type,t.to,t.from),new Ot(e.neutral))}throw new Error(`invalid input for symm ${t}`)}(this.equality.toLazy(t))}prettyPrint(){return`(symm ${this.equality.prettyPrint()})`}toString(){return this.prettyPrint()}},Ge=class extends fe{target;motive;base;constructor(t,e,n){super(),this.target=t,this.motive=e,this.base=n}valOf(t){return function(t,e,n){const r=t.now();if(r instanceof te)return n;if(r instanceof oe){const s=r.type.now();if(s instanceof Jt){const i=s.type,a=s.from,o=s.to,c=r.neutral;return new oe(J(J(e,o),t),new Lt(c,new pt(new Gt("to",i,new B((t=>new Gt("p",new Jt(i,a,t),new B((t=>new ce)))))),e),new pt(J(J(e,a),new te(a)),n)))}}throw new Error(`invalid input for indEqual ${[t,e,n]}`)}(this.target.toLazy(t),this.motive.toLazy(t),this.base.toLazy(t))}prettyPrint(){return`(ind-= ${this.target.prettyPrint()} \n ${this.motive.prettyPrint()} \n ${this.base.prettyPrint()})`}toString(){return this.prettyPrint()}},Xe=class extends fe{type;length;constructor(t,e){super(),this.type=t,this.length=e}valOf(t){return new ee(this.type.toLazy(t),this.length.toLazy(t))}prettyPrint(){return`(Vec ${this.type.prettyPrint()} ${this.length.prettyPrint()})`}toString(){return this.prettyPrint()}},Ke=class extends fe{head;tail;constructor(t,e){super(),this.head=t,this.tail=e}valOf(t){return new re(this.head.toLazy(t),this.tail.toLazy(t))}prettyPrint(){return`(vec:: ${this.head.prettyPrint()} ${this.tail.prettyPrint()})`}toString(){return this.prettyPrint()}},Ye=class extends fe{valOf(t){return new ne}prettyPrint(){return"vecnil"}toString(){return this.prettyPrint()}},Ze=class extends fe{vec;constructor(t){super(),this.vec=t}valOf(t){return function(t){const e=t.now();if(e instanceof re)return e.head;if(e instanceof oe){const t=e.type.now();if(t instanceof ee&&t.length.now()instanceof Vt)return new oe(t.entryType,new At(e.neutral))}throw new Error(`invalid input for head ${t}`)}(this.vec.toLazy(t))}prettyPrint(){return`(head ${this.vec.prettyPrint()})`}toString(){return this.prettyPrint()}},je=class extends fe{vec;constructor(t){super(),this.vec=t}valOf(t){return ot(this.vec.toLazy(t))}prettyPrint(){return`(tail ${this.vec.prettyPrint()})`}toString(){return this.prettyPrint()}},We=class extends fe{length;target;motive;base;step;constructor(t,e,n,r,s){super(),this.length=t,this.target=e,this.motive=n,this.base=r,this.step=s}valOf(t){return ut(this.length.toLazy(t),this.target.toLazy(t),this.motive.toLazy(t),this.base.toLazy(t),this.step.toLazy(t))}prettyPrint(){return`ind-Vec ${this.length.prettyPrint()}\n ${this.target.prettyPrint()}\n ${this.motive.prettyPrint()}\n ${this.base.prettyPrint()}\n ${this.step.prettyPrint()}`}toString(){return this.prettyPrint()}},Je=class extends fe{left;right;constructor(t,e){super(),this.left=t,this.right=e}valOf(t){return new se(this.left.toLazy(t),this.right.toLazy(t))}prettyPrint(){return`(Either ${this.left.prettyPrint()} ${this.right.prettyPrint()})`}toString(){return this.prettyPrint()}},tn=class extends fe{value;constructor(t){super(),this.value=t}valOf(t){return new ie(this.value.toLazy(t))}prettyPrint(){return`(left ${this.value.prettyPrint()})`}toString(){return this.prettyPrint()}},en=class extends fe{value;constructor(t){super(),this.value=t}valOf(t){return new ae(this.value.toLazy(t))}prettyPrint(){return`(right ${this.value.prettyPrint()})`}toString(){return this.prettyPrint()}},nn=class extends fe{target;motive;baseLeft;baseRight;constructor(t,e,n,r){super(),this.target=t,this.motive=e,this.baseLeft=n,this.baseRight=r}valOf(t){return function(t,e,n,r){const s=t.now();if(s instanceof ie)return J(n,s.value);if(s instanceof ae)return J(r,s.value);if(s instanceof oe){const i=s.type.now();if(i instanceof se){const a=i.leftType,o=i.rightType,c=new Gt("x",new se(a,o),new B((t=>new ce)));return new oe(J(e,t),new Rt(s.neutral,new pt(c,e),new pt(new Gt("x",a,new B((t=>J(e,new ie(t))))),n),new pt(new Gt("x",o,new B((t=>J(e,new ae(t))))),r)))}}throw new Error(`invalid input for indEither: ${[t,e,n,r]}`)}(this.target.toLazy(t),this.motive.toLazy(t),this.baseLeft.toLazy(t),this.baseRight.toLazy(t))}prettyPrint(){return`(ind-Either ${this.target.prettyPrint()} \n ${this.motive.prettyPrint()} \n ${this.baseLeft.prettyPrint()} \n ${this.baseRight.prettyPrint()})`}toString(){return this.prettyPrint()}},rn=class extends fe{loc;type;constructor(t,e){super(),this.loc=t,this.type=e}valOf(t){return new oe(this.type.toLazy(t),new yt(this.loc,this.type.toLazy(t)))}prettyPrint(){return`TODO ${this.type.prettyPrint()}`}toString(){return this.prettyPrint()}},sn=class extends fe{fun;arg;constructor(t,e){super(),this.fun=t,this.arg=e}valOf(t){return J(this.fun.toLazy(t),this.arg.toLazy(t))}prettyPrint(){return`(${this.fun.prettyPrint()} ${this.arg.prettyPrint()})`}toString(){return this.prettyPrint()}};class an extends fe{name;constructor(t){super(),this.name=t}valOf(t){if(C(this.name))return function(t,e){if(t.has(e))return t.get(e);throw new Error(`Variable ${e} not found in environment`)}(t,this.name);throw new Error("{this.name} is not a valid variable name")}prettyPrint(){return this.name}toString(){return this.prettyPrint()}}function on(t,e){return ln(0,new Map,new Map,t,e)}const cn=-1;function un(t,e,n){return new Map([[e,n],...t])}function hn(t,e){return e.has(t)?e.get(t):cn}function ln(t,e,n,r,s){if(r instanceof an&&s instanceof an){const t=r.name,i=s.name;if(C(t)&&C(i)){const r=hn(t,e),s=hn(i,n);return r!==cn&&s!==cn?r===s:r===cn&&s===cn&&t===i}return!1}return r instanceof _e&&s instanceof _e?r.sym===s.sym:r instanceof be&&s instanceof be||r instanceof ke&&s instanceof ke?ln(t,e,n,r.type,s.type)&&ln(t+1,un(e,r.name,t),un(n,s.name,t),r.body,s.body):r instanceof Ne&&s instanceof Ne?ln(t+1,un(e,r.param,t),un(n,s.param,t),r.body,s.body):r instanceof we&&s instanceof we&&r.type instanceof Me&&s.type instanceof Me||(r instanceof sn&&s instanceof sn?ln(t,e,n,r.fun,s.fun)&&ln(t,e,n,r.arg,s.arg):r instanceof ye&&s instanceof ye||r instanceof de&&s instanceof de||r instanceof me&&s instanceof me||r instanceof xe&&s instanceof xe||r instanceof Me&&s instanceof Me||r instanceof qe&&s instanceof qe||r instanceof Ae&&s instanceof Ae||r instanceof Ye&&s instanceof Ye||r instanceof Re&&s instanceof Re||(r instanceof we&&s instanceof we?ln(t,e,n,r.type,s.type)&&ln(t,e,n,r.expr,s.expr):r instanceof Ie&&s instanceof Ie?ln(t,e,n,r.elemType,s.elemType):r instanceof ge&&s instanceof ge?ln(t,e,n,r.n,s.n):r instanceof ve&&s instanceof ve||r instanceof Ee&&s instanceof Ee||r instanceof Pe&&s instanceof Pe?ln(t,e,n,r.target,s.target)&&ln(t,e,n,r.base,s.base)&&ln(t,e,n,r.step,s.step):r instanceof Te&&s instanceof Te?ln(t,e,n,r.target,s.target)&&ln(t,e,n,r.motive,s.motive)&&ln(t,e,n,r.base,s.base)&&ln(t,e,n,r.step,s.step):r instanceof Se&&s instanceof Se?ln(t,e,n,r.first,s.first)&&ln(t,e,n,r.second,s.second):r instanceof $e&&s instanceof $e||r instanceof Oe&&s instanceof Oe?ln(t,e,n,r.pair,s.pair):r instanceof Le&&s instanceof Le?ln(t,e,n,r.head,s.head)&&ln(t,e,n,r.tail,s.tail):r instanceof Be&&s instanceof Be?ln(t,e,n,r.target,s.target)&&ln(t,e,n,r.base,s.base)&&ln(t,e,n,r.step,s.step):r instanceof Ce&&s instanceof Ce?ln(t,e,n,r.target,s.target)&&ln(t,e,n,r.motive,s.motive)&&ln(t,e,n,r.base,s.base)&&ln(t,e,n,r.step,s.step):r instanceof Ue&&s instanceof Ue?ln(t,e,n,r.target,s.target)&&ln(t,e,n,r.motive,s.motive):r instanceof He&&s instanceof He?ln(t,e,n,r.type,s.type)&&ln(t,e,n,r.left,s.left)&&ln(t,e,n,r.right,s.right):r instanceof De&&s instanceof De?ln(t,e,n,r.type,s.type):r instanceof ze&&s instanceof ze?ln(t,e,n,r.target,s.target)&&ln(t,e,n,r.motive,s.motive)&&ln(t,e,n,r.base,s.base):r instanceof Qe&&s instanceof Qe?ln(t,e,n,r.left,s.left)&&ln(t,e,n,r.right,s.right):r instanceof Fe&&s instanceof Fe?ln(t,e,n,r.target,s.target)&&ln(t,e,n,r.base,s.base)&&ln(t,e,n,r.fun,s.fun):r instanceof Ve&&s instanceof Ve?ln(t,e,n,r.equality,s.equality):r instanceof Ge&&s instanceof Ge?ln(t,e,n,r.target,s.target)&&ln(t,e,n,r.motive,s.motive)&&ln(t,e,n,r.base,s.base):r instanceof Xe&&s instanceof Xe?ln(t,e,n,r.type,s.type)&&ln(t,e,n,r.length,s.length):r instanceof Ke&&s instanceof Ke?ln(t,e,n,r.head,s.head)&&ln(t,e,n,r.tail,s.tail):r instanceof Ze&&s instanceof Ze||r instanceof je&&s instanceof je?ln(t,e,n,r.vec,s.vec):r instanceof We&&s instanceof We?ln(t,e,n,r.length,s.length)&&ln(t,e,n,r.target,s.target)&&ln(t,e,n,r.motive,s.motive)&&ln(t,e,n,r.base,s.base)&&ln(t,e,n,r.step,s.step):r instanceof Je&&s instanceof Je?ln(t,e,n,r.left,s.left)&&ln(t,e,n,r.right,s.right):r instanceof tn&&s instanceof tn||r instanceof en&&s instanceof en?ln(t,e,n,r.value,s.value):r instanceof nn&&s instanceof nn?ln(t,e,n,r.target,s.target)&&ln(t,e,n,r.motive,s.motive)&&ln(t,e,n,r.baseLeft,s.baseLeft)&&ln(t,e,n,r.baseRight,s.baseRight):r instanceof rn&&s instanceof rn&&(function(t,e){return t.startLine===e.startLine&&t.startColumn===e.startColumn&&t.endLine===e.endLine&&t.endColumn===e.endColumn}(r.loc,s.loc)&&ln(t,e,n,r.type,s.type))))}function pn(t,e){t.forInfo}function fn(t,e){const n=t.get(e);return n||e}function wn(t,e,n){return new Map([[e,n],...t])}function yn(t,e,n,r){const s=n.readBackType(t),i=r.readBackType(t);return on(s,i)?new S(void 0):new $(e,new _([`Expected ${i} but got ${s}`]))}function dn(t,e,n,r,s){return on(lt(t,n,r),lt(t,n,s))?new S(void 0):new $(e,new _([`The terms ${r} and ${s} are not the same ${n}.`]))}function mn(t){return gn(t.split(""))}function gn(t){return 0===t.length||(e=t[0],!(!/^[a-zA-Z]$/.test(e)&&"-"!==t[0])&&gn(t.slice(1)));var e}function vn(t,e,n){return new Er(t.location,t,e,n)}class En{source;startLine;startColumn;endLine;endColumn;constructor(t,e,n,r,s){this.source=t,this.startLine=e,this.startColumn=n,this.endLine=r,this.endColumn=s}}class Pn{start;end;source;constructor(t,e,n){this.start=t,this.end=e,this.source=n}}let Tn=class{syntax;forInfo;constructor(t,e){this.syntax=t,this.forInfo=e}locationToSrcLoc(){return new En(this.syntax.source,this.syntax.start.line,this.syntax.start.column,this.syntax.end.line,this.syntax.end.column)}toString(){return`${this.syntax.source}:${this.syntax.start.line}:${this.syntax.start.column}`}};function bn(t){return new Tn(t.syntax,!1)}class Nn{static synthNat(t,e){return new S(new we(new ye,new de))}static synthUniverse(t,e,n){return new $(n,new _(["U is a type, but it does not have a type."]))}static synthArrow(t,e,n,r,s,i){if(0===i.length){const n=M(t,s,"x"),i=new O("Aout"),a=new O("Bout");return L([[i,()=>r.check(t,e,new ce)],[a,()=>s.check(W(t,n,D(t,i.value)),e,new ce)]],(()=>new S(new we(new ye,new be(n,i.value,a.value)))))}{const[a,...o]=i,c=M(t,vn(s,a,o),"x"),u=new O("Aout"),h=new O("tout");return L([[u,()=>r.check(t,e,new ce)],[h,()=>new Cn(bn(n),s,a,o).check(W(t,c,D(t,u.value)),e,new ce)]],(()=>new S(new we(new ye,new be(c,u.value,h.value)))))}}static synthPi(t,e,n,r,s){if(1===r.length){const[n,i]=[r[0].binder,r[0].type],a=q(t,n.varName),o=(n.location,new O("Aout")),c=new O("Bout");return L([[o,()=>i.check(t,e,new ce)],[c,()=>s.check(W(t,a,D(t,o.value)),wn(e,n.varName,a),new ce)]],(()=>(o.value,new S(new we(new ye,new be(a,o.value,c.value))))))}if(r.length>1){const[i,...a]=r,[o,c]=[i.binder,i.type],u=(o.location,o.varName),h=q(t,u),l=new O("Aout"),p=new O("Bout");return L([[l,()=>c.check(t,e,new ce)],[p,()=>new Rn(bn(n),a,s).check(W(t,h,D(t,l.value)),wn(e,u,h),new ce)]],(()=>(l.value,new S(new we(new ye,new be(h,l.value,p.value))))))}throw new Error("Invalid number of binders in Pi type")}static synthZero(t,e){return new S(new we(new de,new me))}static synthAdd1(t,e,n){const r=new O("nout");return L([[r,()=>n.check(t,e,new Qt)]],(()=>new S(new we(new de,new ge(r.value)))))}static synthWhichNat(t,e,n,r,s){const i=new O("tgtout"),a=new O("bout"),o=new O("sout");let c=q(t,"n_minus_1");return L([[i,()=>n.check(t,e,new Qt)],[a,()=>r.synth(t,e)],[o,()=>s.check(t,e,new Gt(c,new Qt,new I(V(t),c,a.value.type)))]],(()=>new S(new we(a.value.type,new ve(i.value,new we(a.value.type,a.value.expr),o.value)))))}static synthIterNat(t,e,n,r,s){const i=new O("tgtout"),a=new O("bout"),o=new O("sout");return L([[i,()=>n.check(t,e,new Qt)],[a,()=>r.synth(t,e)],[o,()=>s.check(t,e,(()=>{const e=q(t,"old");return D(t,new be(e,a.value.type,a.value.type))})())]],(()=>new S(new we(a.value.type,new Ee(i.value,new we(a.value.type,a.value.expr),o.value)))))}static synthRecNat(t,e,n,r,s){const i=new O("tgtout"),a=new O("bout"),o=new O("sout");return L([[i,()=>n.check(t,e,new Qt)],[a,()=>r.synth(t,e)],[o,()=>s.check(t,e,(()=>{const e=q(t,"n_minus_1"),n=q(t,"old");return D(t,new be(e,new de,new be(n,a.value.type,a.value.type)))})())]],(()=>new S(new we(a.value.type,new Pe(i.value,new we(a.value.type,a.value.expr),o.value)))))}static synthIndNat(t,e,n,r,s,i){const a=new O("tgtout"),o=new O("motout"),c=new O("motval"),u=new O("bout"),h=new O("sout");return L([[a,()=>n.check(t,e,new Qt)],[o,()=>r.check(t,e,new Gt("n",new Qt,new B((t=>new ce))))],[c,()=>new S(D(t,o.value))],[u,()=>s.check(t,e,J(c.value,new Ft))],[h,()=>i.check(t,e,new Gt("n_minus_1",new Qt,new B((t=>new Gt("ih",J(c.value,t),new B((e=>J(c.value,new Vt(t)))))))))]],(()=>new S(new we(new sn(o.value,a.value),new Te(a.value,o.value,u.value,h.value)))))}static synthAtom(t,e){return new S(new we(new ye,new xe))}static synthPair(t,e,n,r){const s=q(t,"a"),i=new O("Aout"),a=new O("Dout");return L([[i,()=>n.check(t,e,new ce)],[a,()=>r.check(W(t,s,D(t,i.value)),e,new ce)]],(()=>new S(new we(new ye,new ke(s,i.value,a.value)))))}static synthSigma(t,e,n,r,s){if(1===r.length){const[n,i]=[r[0].binder,r[0].type],a=q(t,n.varName),o=(n.location,new O("Aout")),c=new O("Dout");return L([[o,()=>i.check(t,e,new ce)],[c,()=>s.check(W(t,a,D(t,o.value)),wn(e,n.varName,a),new ce)]],(()=>(o.value,new S(new we(new ye,new ke(a,o.value,c.value))))))}if(r.length>1){const[i,...a]=r,[o,c]=[i.binder,i.type],u=(o.location,o.varName),h=q(t,u),l=new O("Aout"),p=new O("Dout");return L([[l,()=>c.check(t,e,new ce)],[p,()=>new Mn(bn(n),a,s).check(W(t,h,D(t,l.value)),wn(e,u,h),new ce)]],(()=>(l.value,new S(new we(new ye,new ke(h,l.value,p.value))))))}throw new Error("Invalid number of binders in Sigma type")}static synthCar(t,e,n,r){const s=new O("p_rst");return L([[s,()=>r.synth(t,e)]],(()=>{const e=D(t,s.value.type);return e instanceof Kt?new S(new we(e.carType.readBackType(t),new $e(s.value.expr))):new $(n,new _([`car requires a Pair type, but was used as a: ${e}.`]))}))}static synthCdr(t,e,n,r){const s=new O("pout");return L([[s,()=>r.synth(t,e)]],(()=>{const e=D(t,s.value.type);if(e instanceof Kt){const[n,r,i]=[e.carName,e.carType,e.cdrType];return new S(new we(i.valOfClosure(rt(D(t,s.value.expr))).readBackType(t),new Oe(s.value.expr)))}return new $(n,new _([`cdr requires a Pair type, but was used as a: ${e}.`]))}))}static synthQuote(t,e,n,r){return mn(r)?new S(new we(new xe,new _e(r))):new $(n,new _([`Invalid atom: ${r}. Atoms consist of letters and hyphens.`]))}static synthTrivial(t,e){return new S(new we(new ye,new Re))}static synthSole(t,e){return new S(new we(new Re,new qe))}static synthIndList(t,e,n,r,s,i,a){const o=new O("tgtout"),c=new O("motout"),u=new O("motval"),h=new O("bout"),l=new O("sout");return L([[o,()=>r.synth(t,e)]],(()=>{const[r,p]=[o.value.type,o.value.expr],f=D(t,r);if(f instanceof Zt){const n=f.entryType;return L([[c,()=>s.check(t,e,new Gt("xs",new Zt(n),new I(V(t),"xs",new ye)))],[u,()=>new S(D(t,c.value))],[h,()=>i.check(t,e,J(u.value,new jt))],[l,()=>a.check(t,e,new Gt("e",n,new B((t=>new Gt("es",new Zt(n),new B((e=>new Gt("ih",J(u.value,e),new B((n=>J(u.value,new Wt(t,e))))))))))))]],(()=>new S(new we(new sn(c.value,p),new Ce(p,c.value,h.value,l.value)))))}return new $(n,new _([`Not a List: ${f.readBackType(t)}.`]))}))}static synthRecList(t,e,n,r,s,i){const a=new O("tgtout");return L([[a,()=>r.synth(t,e)]],(()=>{const[r,o]=[a.value.type,a.value.expr],c=D(t,r);if(c instanceof Zt){const n=c.entryType,r=new O("bout"),a=new O("btval"),u=new O("sout");return L([[r,()=>s.synth(t,e)],[a,()=>new S(D(t,r.value.type))],[u,()=>i.check(t,e,new Gt("e",n,new B((t=>new Gt("es",new Zt(n),new B((t=>new Gt("ih",a.value,new B((t=>a.value))))))))))]],(()=>new S(new we(r.value.type,new Be(o,new we(r.value.type,r.value.expr),u.value)))))}return new $(n,new _([`Not a List: ${c.readBackType(t)}.`]))}))}static synthList(t,e,n){const r=new O("Eout");return L([[r,()=>n.entryType.check(t,e,new ce)]],(()=>new S(new we(new ye,new Ie(r.value)))))}static synthListCons(t,e,n,r){const s=new O("eout"),i=new O("esout");return L([[s,()=>n.synth(t,e)],[i,()=>r.check(t,e,D(t,new Ie(s.value.type)))]],(()=>new S(new we(new Ie(s.value.type),new Le(s.value.expr,i.value)))))}static synthAbsurd(t,e,n){return new S(new we(new ye,new Me))}static synthIndAbsurd(t,e,n){const r=new O("tgtout"),s=new O("motout");return L([[r,()=>n.target.check(t,e,new pe)],[s,()=>n.motive.check(t,e,new ce)]],(()=>new S(new we(s.value,new Ue(r.value,s.value)))))}static synthEqual(t,e,n,r,s){const i=new O("Aout"),a=new O("Av"),o=new O("from_out"),c=new O("to_out");return L([[i,()=>n.check(t,e,new ce)],[a,()=>new S(D(t,i.value))],[o,()=>r.check(t,e,a.value)],[c,()=>s.check(t,e,a.value)]],(()=>new S(new we(new ye,new He(i.value,o.value,c.value)))))}static synthReplace(t,e,n,r,s,i){const a=new O("tgt_rst"),o=new O("motout"),c=new O("bout");return L([[a,()=>r.synth(t,e)]],(()=>{const r=D(t,a.value.type);if(r instanceof Jt){const[n,u,h]=[r.type,r.from,r.to];return L([[o,()=>s.check(t,e,new Gt("x",n,new B((t=>new ce))))],[c,()=>i.check(t,e,J(D(t,o.value),u))]],(()=>new S(new we(J(D(t,o.value),h).readBackType(t),new ze(a.value.expr,o.value,c.value)))))}return new $(n,new _([`Expected an expression with = type, but the type was: ${a.value.type}.`]))}))}static synthTrans(t,e,n,r,s){const i=new O("p1_rst"),a=new O("p2_rst");return L([[i,()=>r.synth(t,e)],[a,()=>s.synth(t,e)]],(()=>{const e=D(t,i.value.type),r=D(t,a.value.type);if(e instanceof Jt&&r instanceof Jt){const[s,o,c]=[e.type,e.from,e.to],[u,h,l]=[r.type,r.from,r.to];return L([[new O("_"),()=>yn(t,n,s,u)],[new O("_"),()=>dn(t,n,s,c,h)]],(()=>new S(new we(new Jt(s,o,l).readBackType(t),new Qe(i.value.expr,a.value.expr)))))}return new $(n,new _([`Expected =, got ${e} and ${r}.`]))}))}static synthCong(t,e,n,r,s){const i=new O("bout"),a=new O("f_rst");return L([[i,()=>r.synth(t,e)],[a,()=>s.synth(t,e)]],(()=>{const e=D(t,i.value.type),r=D(t,a.value.type);if(e instanceof Jt){const[s,o,c]=[e.type,e.from,e.to];if(r instanceof Gt){const[e,u,h]=[r.argName,r.argType,r.resultType],l=new O("ph"),p=new O("Cv"),f=new O("fv");return L([[l,()=>yn(t,n,s,u)],[p,()=>new S(h.valOfClosure(o))],[f,()=>new S(D(t,a.value.expr))]],(()=>new S(new we(new He(p.value.readBackType(t),lt(t,p.value,J(f.value,o)),lt(t,p.value,J(f.value,c))),new Fe(i.value.expr,p.value.readBackType(t),a.value.expr)))))}return new $(n,new _([`Expected a function type, got ${r.readBackType(t)}.`]))}return new $(n,new _([`Expected an = type, got ${e.readBackType(t)}.`]))}))}static synthSymm(t,e,n,r){const s=new O("eout");return L([[s,()=>r.synth(t,e)]],(()=>{const e=D(t,s.value.type);if(e instanceof Jt){const[n,r,i]=[e.type,e.from,e.to];return new S(new we(new Jt(n,i,r).readBackType(t),new Ve(s.value.expr)))}return new $(n,new _([`Expected an = type, got ${e.readBackType(t)}.`]))}))}static synthIndEqual(t,e,n,r,s,i){const a=new O("tgtout"),o=new O("motout"),c=new O("motv"),u=new O("baseout");return L([[a,()=>r.synth(t,e)]],(()=>{const r=D(t,a.value.type);if(r instanceof Jt){const[n,h,l]=[r.type,r.from,r.to];return L([[o,()=>s.check(t,e,new Gt("to",n,new B((t=>new Gt("p",new Jt(n,h,t),new B((t=>new ce)))))))],[c,()=>new S(D(t,o.value))],[u,()=>i.check(t,e,J(J(c.value,h),new te(h)))]],(()=>new S(new we(J(J(c.value,l),D(t,a.value.expr)).readBackType(t),new Ge(a.value.expr,o.value,u.value)))))}return new $(n,new _([`Expected evidence of equality, got ${r.readBackType(t)}.`]))}))}static synthVec(t,e,n,r){const s=new O("tout"),i=new O("lenout");return L([[s,()=>n.check(t,e,new ce)],[i,()=>r.check(t,e,new Qt)]],(()=>new S(new we(new ye,new Xe(s.value,i.value)))))}static synthHead(t,e,n,r){const s=new O("vout");return L([[s,()=>r.synth(t,e)]],(()=>{const e=D(t,s.value.type).now();if(e instanceof ee){const[r,i]=[e.entryType,e.length];return i.now()instanceof Vt?new S(new we(r.readBackType(t),new Ze(s.value.expr))):new $(n,new _([`Expected a Vec with add1 at the top of the length, got ${lt(t,new Qt,i)}.`]))}return new $(n,new _([`Expected a Vec, got ${e.readBackType(t)}.`]))}))}static synthTail(t,e,n,r){const s=new O("vout");return L([[s,()=>r.synth(t,e)]],(()=>{const e=D(t,s.value.type).now();if(e instanceof ee){const[r,i]=[e.entryType,e.length],a=i.now();if(a instanceof Vt){const e=a.smaller;return new S(new we(new Xe(r.readBackType(t),lt(t,new Qt,e)),new je(s.value.expr)))}return new $(n,new _([`Expected a Vec with add1 at the top of the length, got ${lt(t,new Qt,i)}.`]))}return new $(n,new _([`Expected a Vec, got ${e.readBackType(t)}.`]))}))}static synthIndVec(t,e,n,r,s,i,a,o){const c=new O("lenout"),u=new O("lenv"),h=new O("vecout"),l=new O("motout"),p=new O("motval"),f=new O("bout"),w=new O("sout");return L([[c,()=>r.check(t,e,new Qt)],[u,()=>new S(D(t,c.value))],[h,()=>s.synth(t,e)]],(()=>{const r=D(t,h.value.type);if(r instanceof ee){const[s,y]=[r.entryType,r.length];return L([[new O("_"),()=>dn(t,n,new Qt,u.value,y)],[l,()=>i.check(t,e,new Gt("k",new Qt,new B((t=>new Gt("es",new ee(s,t),new B((t=>new ce)))))))],[p,()=>new S(D(t,l.value))],[f,()=>a.check(t,e,J(J(p.value,new Ft),new ne))],[w,()=>o.check(t,e,ct(s,p.value))]],(()=>new S(new we(new sn(new sn(l.value,c.value),h.value.expr),new We(c.value,h.value.expr,l.value,f.value,w.value)))))}return new $(n,new _([`Expected a Vec, got ${r.readBackType(t)}.`]))}))}static synthEither(t,e,n,r){const s=new O("Lout"),i=new O("Rout");return L([[s,()=>n.check(t,e,new ce)],[i,()=>r.check(t,e,new ce)]],(()=>new S(new we(new ye,new Je(s.value,i.value)))))}static synthIndEither(t,e,n,r,s,i,a){const o=new O("tgtout"),c=new O("motout"),u=new O("motval"),h=new O("lout"),l=new O("rout");return L([[o,()=>r.synth(t,e)]],(()=>{const r=D(t,o.value.type);if(r instanceof se){const[n,p]=[r.leftType,r.rightType];return L([[c,()=>s.check(t,e,new Gt("x",new se(n,p),new B((t=>new ce))))],[u,()=>new S(D(t,c.value))],[h,()=>i.check(t,e,new Gt("x",n,new B((t=>J(u.value,new ie(t))))))],[l,()=>a.check(t,e,new Gt("x",p,new B((t=>J(u.value,new ae(t))))))]],(()=>new S(new we(new sn(c.value,o.value.expr),new nn(o.value.expr,c.value,h.value,l.value)))))}return new $(n,new _([`Expected an Either, but got a ${r.readBackType(t)}.`]))}))}static synthThe(t,e,n,r){const s=new O("t_out"),i=new O("e_out");return L([[s,()=>n.isType(t,e)],[i,()=>r.check(t,e,D(t,s.value))]],(()=>new S(new we(s.value,i.value))))}static synthApplication(t,e,n,r,s,i){if(0===i.length){const i=new O("fout");return L([[i,()=>r.synth(t,e)]],(()=>{const r=D(t,i.value.type);if(r instanceof Gt){const[n,a,o]=[r.argName,r.argType,r.resultType],c=new O("argout");return L([[c,()=>s.check(t,e,a)]],(()=>new S(new we(o.valOfClosure(D(t,c.value)).readBackType(t),new sn(i.value.expr,c.value)))))}return new $(n,new _([`Not a function type: ${r.readBackType(t)}.`]))}))}{const a=new O("appout");return L([[a,()=>new Er(bn(n),r,s,i.slice(0,i.length-1)).synth(t,e)]],(()=>{const r=D(t,a.value.type);if(r instanceof Gt){const[n,s,o]=[r.argName,r.argType,r.resultType],c=new O("fout");return L([[c,()=>i[i.length-1].check(t,e,s)]],(()=>new S(new we(o.valOfClosure(D(t,c.value)).readBackType(t),new sn(a.value.expr,c.value)))))}return new $(n,new _([`Not a function type: ${r.readBackType(t)}.`]))}))}}static synthName(t,e,n,r){const s=fn(e,r),i=new O("x_tv");return L([[i,()=>j(t,0,s)]],(()=>(t.get(s),new S(new we(i.value.readBackType(t),new an(s))))))}static synthNumber(t,e,n,r){if(0===r)return new S(new we(new de,new me));if(r>0){const s=new O("n_1_out");return L([[s,()=>new Yn(n,r-1).check(t,e,new Qt)]],(()=>new S(new we(new de,new ge(s.value)))))}return new $(n,new _([`Expected a positive number, got ${r}.`]))}}class xn{location;constructor(t){this.location=t}isType(t,e){const n=new O("ok"),r=this.getType(t,e);return L([[n,()=>r]],(()=>(pn(this.location,n.value),new S(n.value))))}getType(t,e){const n=this.check(t,e,new ce);if(n instanceof S)return n;if(n instanceof $){if(this instanceof Un&&C(this.name)){const e=new O("other-tv");return new L([[e,()=>j(t,this.location,this.name)]],(()=>{new $(this.location,new _([`Expected , but given ${e.value.readBackType(t)}`]))}))}return new $(this.location,new _(["not a type"]))}throw new Error("Invalid checkType")}check(t,e,n){const r=new O("ok"),s=this.checkOut(t,e,n);return L([[r,()=>s]],(()=>new S(r.value)))}synth(t,e){const n=new O("ok");return L([[n,()=>this.synthHelper(t,e)]],(()=>(pn(this.location,n.value.type),new S(n.value))))}checkOut(t,e,n){const r=new O("theT");return L([[r,()=>this.synth(t,e)],[new O("_"),()=>yn(t,this.location,D(t,r.value.type),n)]],(()=>new S(r.value.expr)))}}class _n extends xn{location;type;value;constructor(t,e,n){super(t),this.location=t,this.type=e,this.value=n}synthHelper(t,e){return Nn.synthThe(t,e,this.type,this.value)}findNames(){return this.type.findNames().concat(this.value.findNames())}prettyPrint(){return`(the ${this.type.prettyPrint()} ${this.value.prettyPrint()})`}toString(){return this.prettyPrint()}}class kn extends xn{location;constructor(t){super(t),this.location=t}synthHelper(t,e){return Nn.synthUniverse(t,e,this.location)}findNames(){return[]}getType(t,e){return new S(new ye)}prettyPrint(){return"U"}toString(){return this.prettyPrint()}}class Sn extends xn{location;constructor(t){super(t),this.location=t}synthHelper(t,e){return Nn.synthNat(t,e)}findNames(){return[]}getType(t,e){return new S(new de)}prettyPrint(){return"Nat"}toString(){return this.prettyPrint()}}class $n extends xn{location;constructor(t){super(t),this.location=t}synthHelper(t,e){return Nn.synthZero(t,e)}findNames(){return[]}prettyPrint(){return"zero"}toString(){return this.prettyPrint()}}class On extends xn{location;base;constructor(t,e){super(t),this.location=t,this.base=e}synthHelper(t,e){return Nn.synthAdd1(t,e,this.base)}findNames(){return this.base.findNames()}prettyPrint(){return`(add1 ${this.base.prettyPrint()})`}toString(){return this.prettyPrint()}}class Ln extends xn{location;target;base;step;constructor(t,e,n,r){super(t),this.location=t,this.target=e,this.base=n,this.step=r}synthHelper(t,e){return Nn.synthWhichNat(t,e,this.target,this.base,this.step)}findNames(){return this.target.findNames().concat(this.base.findNames()).concat(this.step.findNames())}prettyPrint(){return`(which-nat ${this.target.prettyPrint()} \n ${this.base.prettyPrint()} \n ${this.step.prettyPrint()})`}toString(){return this.prettyPrint()}}class An extends xn{location;target;base;step;constructor(t,e,n,r){super(t),this.location=t,this.target=e,this.base=n,this.step=r}synthHelper(t,e){return Nn.synthIterNat(t,e,this.target,this.base,this.step)}findNames(){return this.target.findNames().concat(this.base.findNames()).concat(this.step.findNames())}prettyPrint(){return`(iter-nat ${this.target.prettyPrint()} \n ${this.base.prettyPrint()} \n ${this.step.prettyPrint()})`}toString(){return this.prettyPrint()}}class In extends xn{location;target;base;step;constructor(t,e,n,r){super(t),this.location=t,this.target=e,this.base=n,this.step=r}synthHelper(t,e){return Nn.synthRecNat(t,e,this.target,this.base,this.step)}findNames(){return this.target.findNames().concat(this.base.findNames()).concat(this.step.findNames())}prettyPrint(){return`(rec-nat ${this.target.prettyPrint()} \n ${this.base.prettyPrint()} \n ${this.step.prettyPrint()})`}toString(){return this.prettyPrint()}}class Bn extends xn{location;target;motive;base;step;constructor(t,e,n,r,s){super(t),this.location=t,this.target=e,this.motive=n,this.base=r,this.step=s}synthHelper(t,e){return Nn.synthIndNat(t,e,this.target,this.motive,this.base,this.step)}findNames(){return this.target.findNames().concat(this.motive.findNames()).concat(this.base.findNames()).concat(this.step.findNames())}prettyPrint(){return`(ind-nat ${this.target.prettyPrint()} \n ${this.motive.prettyPrint()} \n ${this.base.prettyPrint()} \n ${this.step.prettyPrint()})`}toString(){return this.prettyPrint()}}class Cn extends xn{location;arg1;arg2;args;constructor(t,e,n,r){super(t),this.location=t,this.arg1=e,this.arg2=n,this.args=r}synthHelper(t,e){return Nn.synthArrow(t,e,this.location,this.arg1,this.arg2,this.args)}findNames(){return this.arg1.findNames().concat(this.arg2.findNames()).concat(this.args.flatMap((t=>t.findNames())))}getType(t,e){const[n,r,s]=[this.arg1,this.arg2,this.args];if(0===s.length){const s=M(t,r,"x"),i=new O("Aout"),a=new O("Bout");return L([[i,()=>n.isType(t,e)],[a,()=>r.isType(W(t,s,D(t,i.value)),e)]],(()=>new S(new be(s,i.value,a.value))))}{const[i,...a]=s,o=M(t,vn(r,i,a),"x"),c=new O("Aout"),u=new O("tout");return L([[c,()=>n.isType(t,e)],[u,()=>new Cn(bn(this.location),r,i,a).isType(W(t,o,D(t,c.value)),e)]],(()=>new S(new be(o,c.value,u.value))))}}prettyPrint(){return`(-> ${this.arg1.prettyPrint()} ${this.arg2.prettyPrint()} ${this.args.map((t=>t.prettyPrint())).join(" ")})`}toString(){return this.prettyPrint()}}class Rn extends xn{location;binders;body;constructor(t,e,n){super(t),this.location=t,this.binders=e,this.body=n}synthHelper(t,e){return Nn.synthPi(t,e,this.location,this.binders,this.body)}findNames(){return this.binders.flatMap((t=>U(t))).concat(this.body.findNames())}getType(t,e){const[n,r]=[this.binders,this.body];if(1===n.length){const[s,i]=[n[0].binder,n[0].type],a=q(t,s.varName),o=(s.location,new O("Aout")),c=new O("Aoutv"),u=new O("Bout");return L([[o,()=>i.isType(t,e)],[c,()=>new S(D(t,o.value))],[u,()=>r.isType(W(t,a,c.value),wn(e,s.varName,a))]],(()=>(o.value,new S(new be(a,o.value,u.value)))))}if(n.length>1){const[s,...i]=n,[a,o]=[s.binder.varName,s.type],c=q(t,a),u=(s.binder.location,new O("Aout")),h=new O("Aoutv"),l=new O("Bout");return L([[u,()=>o.isType(t,e)],[h,()=>new S(D(t,u.value))],[l,()=>new Rn(bn(this.location),i,r).isType(W(t,c,h.value),wn(e,s.binder.varName,c))]],(()=>(u.value,new S(new be(c,u.value,l.value)))))}throw new Error("Invalid number of binders in Pi type")}prettyPrint(){return`(Π ${this.binders.map((t=>`(${t.binder.varName} ${t.type.prettyPrint()})`)).join(" ")} \n ${this.body.prettyPrint()})`}toString(){return this.prettyPrint()}}class qn extends xn{location;binders;body;constructor(t,e,n){super(t),this.location=t,this.binders=e,this.body=n}synthHelper(t,e){throw new Error("Method not implemented.")}findNames(){return this.binders.map((t=>t.varName)).concat(this.body.findNames())}checkOut(t,e,n){if(1===this.binders.length){const r=this.body,s=this.binders[0],i=s.varName,a=s.location,o=n.now();if(o instanceof Gt){const n=o.argType,s=o.resultType,a=fn(e,i),c=new O("bout");return L([[c,()=>r.check(W(t,a,n),wn(e,i,a),s.valOfClosure(new oe(n,new wt(a))))]],(()=>(n.readBackType(t),new S(new Ne(a,c.value)))))}return new $(a,new _([`Not a function type: ${o.readBackType(t)}.`]))}return new qn(this.location,[this.binders[0]],new qn(bn(this.location),this.binders.slice(1),this.body)).check(t,e,n)}prettyPrint(){return`(lambda ${this.binders.map((t=>t.varName)).join(" ")} ${this.body.prettyPrint()})`}toString(){return this.prettyPrint()}}class Mn extends xn{location;binders;body;constructor(t,e,n){super(t),this.location=t,this.binders=e,this.body=n}synthHelper(t,e){return Nn.synthSigma(t,e,this.location,this.binders,this.body)}findNames(){return this.binders.flatMap((t=>U(t))).concat(this.body.findNames())}getType(t,e){const[n,r]=[this.binders,this.body];if(1===n.length){const[s,i]=[n[0].binder,n[0].type],a=s.varName,o=q(t,a),c=(s.location,new O("Aout")),u=new O("Aoutv"),h=new O("Dout");return L([[c,()=>i.isType(t,e)],[u,()=>new S(D(t,c.value))],[h,()=>r.isType(W(t,o,u.value),wn(e,a,o))]],(()=>(c.value,new S(new ke(o,c.value,h.value)))))}if(n.length>1){const[[s,i],...a]=[[n[0].binder,n[0].type],n[1],...n.slice(2)],o=s.varName,c=q(t,o),u=(s.location,new O("Aout")),h=new O("Aoutv"),l=new O("Dout");return L([[u,()=>i.isType(t,e)],[h,()=>new S(D(t,u.value))],[l,()=>new Mn(this.location,a,r).isType(W(t,o,h.value),wn(e,o,c))]],(()=>(u.value,new S(new ke(c,u.value,l.value)))))}throw new Error("Invalid number of binders in Sigma type")}prettyPrint(){return`(Σ ${this.binders.map((t=>`(${t.binder.varName} ${t.type.prettyPrint()})`)).join(" ")} \n ${this.body.prettyPrint()})`}toString(){return this.prettyPrint()}}class Un extends xn{location;name;constructor(t,e){super(t),this.location=t,this.name=e}synthHelper(t,e){return Nn.synthName(t,e,this.location,this.name)}findNames(){return[this.name]}prettyPrint(){return this.name}toString(){return this.prettyPrint()}}class Hn extends xn{location;constructor(t){super(t),this.location=t}synthHelper(t,e){return Nn.synthAtom(t,e)}findNames(){return[]}getType(t,e){return new S(new xe)}prettyPrint(){return"Atom"}toString(){return this.prettyPrint()}}class Dn extends xn{location;name;constructor(t,e){super(t),this.location=t,this.name=e}synthHelper(t,e){return Nn.synthQuote(t,e,this.location,this.name)}findNames(){return[]}prettyPrint(){return`'${this.name}`}toString(){return this.prettyPrint()}}class zn extends xn{location;first;second;constructor(t,e,n){super(t),this.location=t,this.first=e,this.second=n}synthHelper(t,e){return Nn.synthPair(t,e,this.first,this.second)}findNames(){return this.first.findNames().concat(this.second.findNames())}getType(t,e){const n=new O("Aout"),r=new O("Dout"),s=M(t,this.second,"x");return L([[n,()=>this.first.isType(t,e)],[r,()=>this.second.isType(W(t,s,D(t,n.value)),e)]],(()=>new S(new ke(s,n.value,r.value))))}prettyPrint(){return`(Pair ${this.first.prettyPrint()} ${this.second.prettyPrint()})`}toString(){return this.prettyPrint()}}class Qn extends xn{location;first;second;constructor(t,e,n){super(t),this.location=t,this.first=e,this.second=n}synthHelper(t,e){throw new Error("Method not implemented.")}findNames(){return this.first.findNames().concat(this.second.findNames())}checkOut(t,e,n){const r=n.now();if(r instanceof Kt){const n=r.carType,s=r.cdrType,i=new O("aout"),a=new O("dout");return L([[i,()=>this.first.check(t,e,n)],[a,()=>this.second.check(t,e,s.valOfClosure(D(t,i.value)))]],(()=>new S(new Se(i.value,a.value))))}return new $(this.location,new _([`cons requires a Pair or Σ type, but was used as a: ${r.readBackType(t)}.`]))}prettyPrint(){return`(cons ${this.first.prettyPrint()} ${this.second.prettyPrint()})`}toString(){return this.prettyPrint()}}class Fn extends xn{location;pair;constructor(t,e){super(t),this.location=t,this.pair=e}synthHelper(t,e){return Nn.synthCar(t,e,this.location,this.pair)}findNames(){return this.pair.findNames()}prettyPrint(){return`(car ${this.pair.prettyPrint()})`}toString(){return this.prettyPrint()}}class Vn extends xn{location;pair;constructor(t,e){super(t),this.location=t,this.pair=e}synthHelper(t,e){return Nn.synthCdr(t,e,this.location,this.pair)}findNames(){return this.pair.findNames()}prettyPrint(){return`(cdr ${this.pair.prettyPrint()})`}toString(){return this.prettyPrint()}}class Gn extends xn{location;constructor(t){super(t),this.location=t}synthHelper(t,e){return Nn.synthTrivial(t,e)}findNames(){return[]}getType(t,e){return new S(new Re)}prettyPrint(){return"Trivial"}toString(){return this.prettyPrint()}}class Xn extends xn{location;constructor(t){super(t),this.location=t}synthHelper(t,e){return Nn.synthSole(t,e)}findNames(){return[]}prettyPrint(){return"Sole"}}class Kn extends xn{location;constructor(t){super(t),this.location=t}synthHelper(t,e){throw new Error("Method not implemented.")}findNames(){return[]}checkOut(t,e,n){const r=n.now();return r instanceof Zt?new S(new Ae):new $(this.location,new _([`nil requires a List type, but was used as a: ${r.readBackType(t)}.`]))}prettyPrint(){return"nil"}toString(){return this.prettyPrint()}}let Yn=class extends xn{location;value;constructor(t,e){super(t),this.location=t,this.value=e}synthHelper(t,e){return Nn.synthNumber(t,e,this.location,this.value)}findNames(){return[]}prettyPrint(){return`${this.value}`}toString(){return this.prettyPrint()}};class Zn extends xn{location;entryType;constructor(t,e){super(t),this.location=t,this.entryType=e}synthHelper(t,e){return Nn.synthList(t,e,this)}findNames(){return this.entryType.findNames()}getType(t,e){const n=new O("Eout");return L([[n,()=>this.entryType.isType(t,e)]],(()=>new S(new Ie(n.value))))}prettyPrint(){return`(List ${this.entryType.prettyPrint()})`}toString(){return this.prettyPrint()}}class jn extends xn{location;x;xs;constructor(t,e,n){super(t),this.location=t,this.x=e,this.xs=n}synthHelper(t,e){return Nn.synthListCons(t,e,this.x,this.xs)}findNames(){return this.x.findNames().concat(this.xs.findNames())}prettyPrint(){return`(:: ${this.x.prettyPrint()} ${this.xs.prettyPrint()})`}toString(){return this.prettyPrint()}}class Wn extends xn{location;target;base;step;constructor(t,e,n,r){super(t),this.location=t,this.target=e,this.base=n,this.step=r}synthHelper(t,e){return Nn.synthRecList(t,e,this.location,this.target,this.base,this.step)}findNames(){return this.target.findNames().concat(this.base.findNames()).concat(this.step.findNames())}prettyPrint(){return`(rec-list ${this.target.prettyPrint()} \n ${this.base.prettyPrint()} \n ${this.step.prettyPrint()})`}toString(){return this.prettyPrint()}}class Jn extends xn{location;target;motive;base;step;constructor(t,e,n,r,s){super(t),this.location=t,this.target=e,this.motive=n,this.base=r,this.step=s}synthHelper(t,e){return Nn.synthIndList(t,e,this.location,this.target,this.motive,this.base,this.step)}findNames(){return this.target.findNames().concat(this.motive.findNames()).concat(this.base.findNames()).concat(this.step.findNames())}prettyPrint(){return`(ind-list ${this.target.prettyPrint()} \n ${this.motive.prettyPrint()} \n ${this.base.prettyPrint()} \n ${this.step.prettyPrint()})`}toString(){return this.prettyPrint()}}class tr extends xn{location;constructor(t){super(t),this.location=t}synthHelper(t,e){return Nn.synthAbsurd(t,e,this)}findNames(){return[]}getType(t,e){return new S(new Me)}prettyPrint(){return"Absurd"}toString(){return this.prettyPrint()}}class er extends xn{location;target;motive;constructor(t,e,n){super(t),this.location=t,this.target=e,this.motive=n}synthHelper(t,e){return Nn.synthIndAbsurd(t,e,this)}findNames(){return this.target.findNames().concat(this.motive.findNames())}prettyPrint(){return`(ind-Absurd \n ${this.target.prettyPrint()} \n ${this.motive.prettyPrint()})`}toString(){return this.prettyPrint()}}class nr extends xn{location;type;left;right;constructor(t,e,n,r){super(t),this.location=t,this.type=e,this.left=n,this.right=r}synthHelper(t,e){return Nn.synthEqual(t,e,this.type,this.left,this.right)}findNames(){return this.type.findNames().concat(this.left.findNames()).concat(this.right.findNames())}getType(t,e){const[n,r,s]=[this.type,this.left,this.right],i=new O("Aout"),a=new O("Av"),o=new O("from_out"),c=new O("to_out");return L([[i,()=>n.isType(t,e)],[a,()=>new S(D(t,i.value))],[o,()=>r.check(t,e,a.value)],[c,()=>s.check(t,e,a.value)]],(()=>new S(new He(i.value,o.value,c.value))))}prettyPrint(){return`(= ${this.type.prettyPrint()} \n ${this.left.prettyPrint()} \n ${this.right.prettyPrint()})`}toString(){return this.prettyPrint()}}class rr extends xn{location;type;constructor(t,e){super(t),this.location=t,this.type=e}findNames(){return this.type.findNames()}synthHelper(t,e){throw new Error("Method not implemented.")}checkOut(t,e,n){const r=n.now();if(r instanceof Jt){const n=r.type,s=r.from,i=r.to,a=new O("cout"),o=new O("val");return L([[a,()=>this.type.check(t,e,n)],[o,()=>new S(D(t,a.value))],[new O("_"),()=>dn(t,this.type.location,n,s,o.value)],[new O("_"),()=>dn(t,this.type.location,n,i,o.value)]],(()=>new S(new De(a.value))))}return new $(this.location,new _([`same requires an Equal type, but was used as a: ${r.readBackType(t)}.`]))}prettyPrint(){return`(same ${this.type.prettyPrint()})`}toString(){return this.prettyPrint()}}class sr extends xn{location;target;motive;base;constructor(t,e,n,r){super(t),this.location=t,this.target=e,this.motive=n,this.base=r}synthHelper(t,e){return Nn.synthReplace(t,e,this.location,this.target,this.motive,this.base)}findNames(){return this.target.findNames().concat(this.motive.findNames()).concat(this.base.findNames())}prettyPrint(){return`(replace ${this.target.prettyPrint()} \n ${this.motive.prettyPrint()} \n ${this.base.prettyPrint()})`}toString(){return this.prettyPrint()}}class ir extends xn{location;left;right;synthHelper(t,e){return Nn.synthTrans(t,e,this.location,this.left,this.right)}constructor(t,e,n){super(t),this.location=t,this.left=e,this.right=n}findNames(){return this.left.findNames().concat(this.right.findNames())}prettyPrint(){return`(trans ${this.left.prettyPrint()} ${this.right.prettyPrint()})`}toString(){return this.prettyPrint()}}class ar extends xn{location;target;fun;constructor(t,e,n){super(t),this.location=t,this.target=e,this.fun=n}synthHelper(t,e){return Nn.synthCong(t,e,this.location,this.target,this.fun)}findNames(){return this.target.findNames().concat(this.fun.findNames())}prettyPrint(){return`(cong ${this.target.prettyPrint()} ${this.fun.prettyPrint()})`}toString(){return this.prettyPrint()}}class or extends xn{location;equality;constructor(t,e){super(t),this.location=t,this.equality=e}synthHelper(t,e){return Nn.synthSymm(t,e,this.location,this.equality)}findNames(){return this.equality.findNames()}prettyPrint(){return`(symm ${this.equality.prettyPrint()})`}toString(){return this.prettyPrint()}}class cr extends xn{location;target;motive;base;constructor(t,e,n,r){super(t),this.location=t,this.target=e,this.motive=n,this.base=r}synthHelper(t,e){return Nn.synthIndEqual(t,e,this.location,this.target,this.motive,this.base)}findNames(){return this.target.findNames().concat(this.motive.findNames()).concat(this.base.findNames())}prettyPrint(){return`(ind-= ${this.target.prettyPrint()} \n ${this.motive.prettyPrint()} \n ${this.base.prettyPrint()})`}toString(){return this.prettyPrint()}}class ur extends xn{location;type;length;constructor(t,e,n){super(t),this.location=t,this.type=e,this.length=n}synthHelper(t,e){return Nn.synthVec(t,e,this.type,this.length)}findNames(){return this.type.findNames().concat(this.length.findNames())}getType(t,e){const n=new O("Eout"),r=new O("lenout");return L([[n,()=>this.type.isType(t,e)],[r,()=>this.length.check(t,e,new Qt)]],(()=>new S(new Xe(n.value,r.value))))}prettyPrint(){return`(Vec ${this.type.prettyPrint()} ${this.length.prettyPrint()})`}toString(){return this.prettyPrint()}}class hr extends xn{location;constructor(t){super(t),this.location=t}synthHelper(t,e){throw new Error("Method not implemented.")}findNames(){return[]}checkOut(t,e,n){const r=n.now();if(r instanceof ee){return r.length.now()instanceof Ft?new S(new Ye):new $(this.location,new _([`vecnil requires a Vec type with length ZERO, but was used as a: \n ${lt(t,new Qt,r.length)}.`]))}return new $(this.location,new _([`vecnil requires a Vec type, but was used as a: ${r.readBackType(t)}.`]))}prettyPrint(){return"vecnil"}toString(){return this.prettyPrint()}}class lr extends xn{location;x;xs;constructor(t,e,n){super(t),this.location=t,this.x=e,this.xs=n}synthHelper(t,e){throw new Error("Method not implemented.")}findNames(){return this.x.findNames().concat(this.xs.findNames())}checkOut(t,e,n){const r=n.now();if(r instanceof ee){const n=r.length.now();if(n instanceof Vt){const s=new O("hout"),i=new O("tout"),a=n.smaller;return L([[s,()=>this.x.check(t,e,r.entryType)],[i,()=>this.xs.check(t,e,new ee(r.entryType,a))]],(()=>new S(new Ke(s.value,i.value))))}return new $(this.location,new _([`vec:: requires a Vec type with length Add1, but was used with a: \n ${lt(t,new Qt,r.length)}.`]))}return new $(this.location,new _([`vec:: requires a Vec type, but was used as a: ${r.readBackType(t)}.`]))}prettyPrint(){return`(vec:: ${this.x.prettyPrint()} ${this.xs.prettyPrint()})`}toString(){return this.prettyPrint()}}class pr extends xn{location;vec;constructor(t,e){super(t),this.location=t,this.vec=e}synthHelper(t,e){return Nn.synthHead(t,e,this.location,this.vec)}findNames(){return this.vec.findNames()}prettyPrint(){return`(head ${this.vec.prettyPrint()})`}toString(){return this.prettyPrint()}}class fr extends xn{location;vec;constructor(t,e){super(t),this.location=t,this.vec=e}synthHelper(t,e){return Nn.synthTail(t,e,this.location,this.vec)}findNames(){return this.vec.findNames()}prettyPrint(){return`(tail ${this.vec.prettyPrint()})`}toString(){return this.prettyPrint()}}class wr extends xn{location;length;target;motive;base;step;constructor(t,e,n,r,s,i){super(t),this.location=t,this.length=e,this.target=n,this.motive=r,this.base=s,this.step=i}synthHelper(t,e){return Nn.synthIndVec(t,e,this.location,this.length,this.target,this.motive,this.base,this.step)}findNames(){return this.length.findNames().concat(this.target.findNames()).concat(this.motive.findNames()).concat(this.base.findNames()).concat(this.step.findNames())}prettyPrint(){return`ind-Vec ${this.length.prettyPrint()}\n ${this.target.prettyPrint()}\n ${this.motive.prettyPrint()}\n ${this.base.prettyPrint()}\n ${this.step.prettyPrint()}`}toString(){return this.prettyPrint()}}class yr extends xn{location;left;right;constructor(t,e,n){super(t),this.location=t,this.left=e,this.right=n}synthHelper(t,e){return Nn.synthEither(t,e,this.left,this.right)}findNames(){return this.left.findNames().concat(this.right.findNames())}getType(t,e){const n=new O("Lout"),r=new O("Rout");return L([[n,()=>this.left.isType(t,e)],[r,()=>this.right.isType(t,e)]],(()=>new S(new Je(n.value,r.value))))}prettyPrint(){return`(Either ${this.left.prettyPrint()} ${this.right.prettyPrint()})`}toString(){return this.prettyPrint()}}class dr extends xn{location;value;constructor(t,e){super(t),this.location=t,this.value=e}synthHelper(t,e){throw new Error("Method not implemented.")}findNames(){return this.value.findNames()}checkOut(t,e,n){const r=n.now();if(r instanceof se){const n=new O("lout");return L([[n,()=>this.value.check(t,e,r.leftType)]],(()=>new S(new tn(n.value))))}return new $(this.location,new _([`left requires an Either type, but was used as a: ${r.readBackType(t)}.`]))}prettyPrint(){return`(left ${this.value.prettyPrint()})`}toString(){return this.prettyPrint()}}class mr extends xn{location;value;constructor(t,e){super(t),this.location=t,this.value=e}synthHelper(t,e){throw new Error("Method not implemented.")}findNames(){return this.value.findNames()}checkOut(t,e,n){const r=n.now();if(r instanceof se){const n=new O("rout");return L([[n,()=>this.value.check(t,e,r.rightType)]],(()=>new S(new en(n.value))))}return new $(this.location,new _([`right requires an Either type, but was used as a: ${r.readBackType(t)}.`]))}prettyPrint(){return`(right ${this.value.prettyPrint()})`}toString(){return this.prettyPrint()}}class gr extends xn{location;target;motive;baseLeft;baseRight;constructor(t,e,n,r,s){super(t),this.location=t,this.target=e,this.motive=n,this.baseLeft=r,this.baseRight=s}synthHelper(t,e){return Nn.synthIndEither(t,e,this.location,this.target,this.motive,this.baseLeft,this.baseRight)}findNames(){return this.target.findNames().concat(this.motive.findNames()).concat(this.baseLeft.findNames()).concat(this.baseRight.findNames())}prettyPrint(){return`(ind-Either ${this.target.prettyPrint()} \n ${this.motive.prettyPrint()} \n ${this.baseLeft.prettyPrint()} \n ${this.baseRight.prettyPrint()})`}toString(){return this.prettyPrint()}}class vr extends xn{location;constructor(t){super(t),this.location=t}synthHelper(t,e){throw new Error("Method not implemented.")}findNames(){return[]}checkOut(t,e,n){const r=n.readBackType(t);return pn(this.location,z(t)),new S(new rn(this.location.locationToSrcLoc(),r))}prettyPrint(){return"TODO"}toString(){return this.prettyPrint()}}class Er extends xn{location;func;arg;args;constructor(t,e,n,r){super(t),this.location=t,this.func=e,this.arg=n,this.args=r}synthHelper(t,e){return Nn.synthApplication(t,e,this.location,this.func,this.arg,this.args)}findNames(){return this.func.findNames().concat(this.arg.findNames()).concat(this.args.flatMap((t=>t.findNames())))}prettyPrint(){return`(${this.func.prettyPrint()} ${this.arg.prettyPrint()} ${this.args.map((t=>t.prettyPrint())).join(" ")})`}toString(){return this.prettyPrint()}}var Pr,Tr;!function(t){t[t.INTEGER=1]="INTEGER",t[t.RATIONAL=2]="RATIONAL",t[t.REAL=3]="REAL",t[t.COMPLEX=4]="COMPLEX"}(Pr||(Pr={}));class br{result;constructor(t){this.result=t}}class Nr extends br{result;value;constructor(t,e){super(t),this.result=t,this.value=e}isSigned(){return!!this.result&&("+"===this.value[0]||"-"===this.value[0])}build(){return Or.build(this.value)}}class xr extends br{result;numerator;denominator;constructor(t,e,n){super(t),this.result=t,this.numerator=e,this.denominator=n}build(){return Lr.build(this.numerator,this.denominator)}}class _r extends br{result;integer;decimal;exponent;constructor(t,e,n,r){super(t),this.result=t,this.integer=e,this.decimal=n,this.exponent=r}build(){if(this.integer?.includes("inf"))return this.integer.includes("-")?Ar.NEG_INFINITY:Ar.INFINITY;if(this.integer?.includes("nan"))return Ar.NAN;let t=(this.exponent?this.exponent.build():Ar.INEXACT_ZERO).coerce(),e=Number((this.integer?this.integer:"0")+"."+(this.decimal?this.decimal:"0"));return e*=Math.pow(10,t),Ar.build(e)}}class kr extends br{result;real;sign;imaginary;constructor(t,e,n,r){super(t),this.result=t,this.real=e,this.sign=n,this.imaginary=r}build(){const t=this.real?this.real.build():Or.EXACT_ZERO,e=this.imaginary.build();return this.sign&&"-"===this.sign?Ir.build(t,e.negate()):Ir.build(t,e)}}function Sr(t){const e=new RegExp("^([+-]?)(\\d+)$").exec(t);return e?new Nr(!0,e[0]):new Nr(!1)}function $r(t,e){const n=Sr(t);if(n.result&&e>=Pr.INTEGER)return n;const r=function(t){if(1!==(t.match(/\//g)||[]).length)return new xr(!1);const e=t.split("/");if(2!==e.length)return new xr(!1);const[n,r]=e,s=Sr(n),i=Sr(r);return s.result&&i.result?new xr(!0,n,r):new xr(!1)}(t);if(r.result&&e>=Pr.RATIONAL)return r;const s=function(t){function e(t){if(function(t){return"+inf.0"===t||"-inf.0"===t||"+nan.0"===t||"-nan.0"===t}(t))return new _r(!0,t);const e=(t.match(/\./g)||[]).length;if(e>1)return new _r(!1);if(0===e){const e=Sr(t);return new _r(e.result,e.value)}const[n,r]=t.split("."),s=Sr(n),i=Sr(r),a=s.result||""===n,o=i.result||""===r;return"+"===n||"-"===n?""===r?new _r(!1):new _r(!0,`${n}0`,t):s.result&&o||a&&i.result?i.result&&i.isSigned()?new _r(!1):new _r(!0,s.value,i.value):new _r(!1)}return 0===(t.match(/[eE]/g)||[]).length?e(t):function(t){const n=t.indexOf("e"),r=t.indexOf("E");if(-1===n&&-1===r)return new _r(!1);const s=-1===n?r:n,i=t.substring(0,s),a=t.substring(s+1);if(""===i||""==a)return new _r(!1);const o=e(i);if(!o.result)return new _r(!1);const c=$r(a,Pr.REAL);return c.result?new _r(!0,o.integer,o.decimal,c):new _r(!1)}(t)}(t);if(s.result&&e>=Pr.REAL)return s;const i=function(t){if((t.match(/i/g)||[]).length<1)return new kr(!1);if("i"!==t[t.length-1])return new kr(!1);const e=t.search(/(?=Pr.COMPLEX?i:new Nr(!1)}class Or{numberType=Pr.INTEGER;value;static EXACT_ZERO=new Or(0n);constructor(t){this.value=t}static build(t,e=!1){const n=BigInt(t);return 0n===n?Or.EXACT_ZERO:new Or(n)}promote(t){switch(t){case Pr.INTEGER:return this;case Pr.RATIONAL:return Lr.build(this.value,1n,!0);case Pr.REAL:return Ar.build(this.coerce(),!0);case Pr.COMPLEX:return Ir.build(this,Or.EXACT_ZERO,!0)}}equals(t){return t instanceof Or&&this.value===t.value}greaterThan(t){return this.value>t.value}negate(){return this===Or.EXACT_ZERO?this:Or.build(-this.value)}multiplicativeInverse(){if(this===Or.EXACT_ZERO)throw new Error("Division by zero");return Lr.build(1n,this.value,!1)}add(t){return Or.build(this.value+t.value)}multiply(t){return Or.build(this.value*t.value)}getBigInt(){return this.value}coerce(){return this.value>Number.MAX_SAFE_INTEGER?1/0:this.value0n===e?t:r(e,t.valueOf()%e.valueOf()),s=r(t,e),i=t<0n?-1n:1n,a=e<0n?-1n:1n,o=i*a;return t*=i,1n!==(e*=a)||n?new Lr(o*t/s,e/s):Or.build(o*t)}getNumerator(){return this.numerator}getDenominator(){return this.denominator}promote(t){switch(t){case Pr.RATIONAL:return this;case Pr.REAL:return Ar.build(this.coerce(),!0);case Pr.COMPLEX:return Ir.build(this,Or.EXACT_ZERO,!0);default:throw new Error("Unable to demote rational")}}equals(t){return t instanceof Lr&&this.numerator===t.numerator&&this.denominator===t.denominator}greaterThan(t){return this.numerator*t.denominator>t.numerator*this.denominator}negate(){return Lr.build(-this.numerator,this.denominator)}multiplicativeInverse(){if(0n===this.numerator)throw new Error("Division by zero");return Lr.build(this.denominator,this.numerator)}add(t){const e=this.numerator*t.denominator+t.numerator*this.denominator,n=this.denominator*t.denominator;return Lr.build(e,n)}multiply(t){const e=this.numerator*t.numerator,n=this.denominator*t.denominator;return Lr.build(e,n)}coerce(){const t=this.numerator<0n?-this.numerator:this.numerator;let e=this.denominator;const n=Number(t/e);if(n>Number.MAX_VALUE)return this.numerator<0n?-1/0:1/0;let r=t%e;for(;r>Number.MAX_SAFE_INTEGER||e>Number.MAX_SAFE_INTEGER;)r/=2n,e/=2n;const s=Number(r)/Number(e);return this.numerator<0n?-(n+s):n+s}toString(){return`${this.numerator}/${this.denominator}`}}class Ar{numberType=Pr.REAL;value;static INEXACT_ZERO=new Ar(0);static INEXACT_NEG_ZERO=new Ar(-0);static INFINITY=new Ar(1/0);static NEG_INFINITY=new Ar(-1/0);static NAN=new Ar(NaN);static build(t,e=!1){return t===1/0?Ar.INFINITY:t===-1/0?Ar.NEG_INFINITY:isNaN(t)?Ar.NAN:0===t?Ar.INEXACT_ZERO:-0===t?Ar.INEXACT_NEG_ZERO:new Ar(t)}constructor(t){this.value=t}promote(t){switch(t){case Pr.REAL:return this;case Pr.COMPLEX:return Ir.build(this,Or.EXACT_ZERO,!0);default:throw new Error("Unable to demote real")}}equals(t){return t instanceof Ar&&this.value===t.value}greaterThan(t){return this.value>t.value}negate(){return Ar.build(-this.value)}multiplicativeInverse(){if(this===Ar.INEXACT_ZERO||this===Ar.INEXACT_NEG_ZERO)throw new Error("Division by zero");return Ar.build(1/this.value)}add(t){return Ar.build(this.value+t.value)}multiply(t){return Ar.build(this.value*t.value)}coerce(){return this.value}toString(){return this===Ar.INFINITY?"+inf.0":this===Ar.NEG_INFINITY?"-inf.0":this===Ar.NAN?"+nan.0":this.value.toString()}}class Ir{numberType=Pr.COMPLEX;real;imaginary;static build(t,e,n=!1){return Ir.simplify(new Ir(t,e),n)}constructor(t,e){this.real=t,this.imaginary=e}static simplify(t,e){return!e&&qr(t.imaginary,Or.EXACT_ZERO)?t.real:t}promote(t){if(t===Pr.COMPLEX)return this;throw new Error("Unable to demote complex")}negate(){return Ir.build(this.real.negate(),this.imaginary.negate())}equals(t){return qr(this.real,t.real)&&qr(this.imaginary,t.imaginary)}greaterThan(t){return Mr(this.real,t.real)&&Mr(this.imaginary,t.imaginary)}multiplicativeInverse(){const t=Ur(Hr(this.real,this.real),Hr(this.imaginary,this.imaginary));return Ir.build(Hr(t.multiplicativeInverse(),this.real),Hr(t.multiplicativeInverse(),this.imaginary.negate()))}add(t){return Ir.build(Ur(this.real,t.real),Ur(this.imaginary,t.imaginary))}multiply(t){const e=(n=Hr(this.real,t.real),r=Hr(this.imaginary,t.imaginary),Ur(n,function(t){return t.negate()}(r)));var n,r;const s=Ur(Hr(this.real,t.imaginary),Hr(this.imaginary,t.real));return Ir.build(e,s)}getReal(){return this.real}getImaginary(){return this.imaginary}coerce(){throw new Error("Cannot coerce a complex number to a javascript number")}toPolar(){const t=this.real.promote(Pr.REAL),e=this.imaginary.promote(Pr.REAL),n=Ar.build(Math.sqrt(t.coerce()*t.coerce()+e.coerce()*e.coerce())),r=Ar.build(Math.atan2(e.coerce(),t.coerce()));return Br.build(n,r)}toString(){return`${this.real}+${this.imaginary}i`}}class Br{magnitude;angle;constructor(t,e){this.magnitude=t,this.angle=e}static build(t,e){return new Br(t,e)}toCartesian(){const t=Ar.build(this.magnitude.coerce()*Math.cos(this.angle.coerce())),e=Ar.build(this.magnitude.coerce()*Math.sin(this.angle.coerce()));return Ir.build(t,e)}}function Cr(t){switch(t.numberType){case Pr.INTEGER:return t;case Pr.RATIONAL:return 1n===t.getDenominator()?Or.build(t.getNumerator()):t;case Pr.REAL:return t;case Pr.COMPLEX:return Ir.build(Cr(t.getReal()),Cr(t.getImaginary()))}}function Rr(t,e){return t.numberType>e.numberType?[t,e.promote(t.numberType)]:t.numberType");return new jr(t)}var e;if(2===t.length){const e=t[0];if(Wr(e)&&function(t){return t.type===Tr.APOSTROPHE||t.type===Tr.BACKTICK||t.type===Tr.HASH_VECTOR||t.type===Tr.COMMA||t.type===Tr.COMMA_AT}(e))return new jr(t)}const n=t[0],r=t[t.length-1];if(Wr(n)&&Wr(r)&&(i=r,(s=n).type===Tr.LEFT_PAREN&&i.type===Tr.RIGHT_PAREN||s.type===Tr.LEFT_BRACKET&&i.type===Tr.RIGHT_BRACKET))return new jr(t);var s,i;const a=new jr(t);throw new Kr("",a.location.start,a,"matching parentheses")}first(){return this.elements[0]}firstToken(){const t=this.first();return Wr(t)?t:t.firstToken()}firstPos(){return this.firstToken().pos}last(){return this.elements[this.elements.length-1]}lastToken(){const t=this.last();return Wr(t)?t:t.lastToken()}lastPos(){return this.lastToken().pos}isParenthesized(){const t=this.first();return Wr(t)&&(t.type===Tr.LEFT_PAREN||t.type===Tr.LEFT_BRACKET)}isSingleIdentifier(){return!this.isParenthesized()&&1===this.length()}unwrap(){return this.isParenthesized()?this.elements.slice(1,this.elements.length-1):this.elements}length(){return this.unwrap().length}toString(){return this.elements.map((t=>t.toString())).join(" ")}}function Wr(t){return t instanceof ts}function Jr(t){return t instanceof jr}class ts{type;lexeme;literal;start;end;pos;endPos;constructor(t,e,n,r,s,i,a){this.type=t,this.lexeme=e,this.literal=n,this.start=r,this.end=s,this.pos=new zr(i,a),this.endPos=new zr(i,a+e.length-1)}convertToken(){switch(this.type){case Tr.APOSTROPHE:return new ts(Tr.QUOTE,this.lexeme,this.literal,this.start,this.end,this.pos.line,this.pos.column);case Tr.BACKTICK:return new ts(Tr.QUASIQUOTE,this.lexeme,this.literal,this.start,this.end,this.pos.line,this.pos.column);case Tr.HASH_VECTOR:return new ts(Tr.VECTOR,this.lexeme,this.literal,this.start,this.end,this.pos.line,this.pos.column);case Tr.COMMA:return new ts(Tr.UNQUOTE,this.lexeme,this.literal,this.start,this.end,this.pos.line,this.pos.column);case Tr.COMMA_AT:return new ts(Tr.UNQUOTE_SPLICING,this.lexeme,this.literal,this.start,this.end,this.pos.line,this.pos.column);default:return this}}toString(){return`${this.lexeme}`}}class es extends SyntaxError{loc;constructor(t,e,n){super(t),this.loc={line:e,column:n}}toString(){return this.message}}class ns extends es{char;constructor(t,e,n){super(`Unexpected character '${n}' (${t}:${e})`,t,e),this.char=n,this.name="UnexpectedCharacterError"}}class rs extends es{constructor(t,e){super(`Unexpected EOF (${t}:${e})`,t,e),this.name="UnexpectedEOFError"}}let ss=new Map([[".",Tr.DOT],["if",Tr.IF],["let",Tr.LET],["cond",Tr.COND],["else",Tr.ELSE],["set!",Tr.SET],["begin",Tr.BEGIN],["delay",Tr.DELAY],["quote",Tr.QUOTE],["export",Tr.EXPORT],["import",Tr.IMPORT],["define",Tr.DEFINE],["lambda",Tr.LAMBDA],["define-syntax",Tr.DEFINE_SYNTAX],["syntax-rules",Tr.SYNTAX_RULES]]);class is{source;tokens;start=0;current=0;line=1;col=0;constructor(t){this.source=t,this.tokens=[]}isAtEnd(){return this.current>=this.source.length}advance(){return this.col++,this.source.charAt(this.current++)}jump(){this.start=this.current,this.col++,this.current++}addToken(t,e=null){const n=this.source.substring(this.start,this.current);this.tokens.push(new ts(t,n,e,this.start,this.current,this.line,this.col))}scanTokens(){for(;!this.isAtEnd();)this.start=this.current,this.scanToken();return this.tokens.push(new ts(Tr.EOF,"",null,this.start,this.current,this.line,this.col)),this.tokens}scanToken(){const t=this.advance();switch(t){case"(":this.addToken(Tr.LEFT_PAREN);break;case")":this.addToken(Tr.RIGHT_PAREN);break;case"[":this.addToken(Tr.LEFT_BRACKET);break;case"]":this.addToken(Tr.RIGHT_BRACKET);break;case"'":this.addToken(Tr.APOSTROPHE);break;case"`":this.addToken(Tr.BACKTICK);break;case",":if(this.match("@")){this.addToken(Tr.COMMA_AT);break}this.addToken(Tr.COMMA);break;case"#":if(this.match("t")||this.match("f"))this.booleanToken();else if(this.match("|"))this.comment();else if(this.match(";"))this.addToken(Tr.HASH_SEMICOLON);else{if("("!==this.peek()&&"["!==this.peek())throw new ns(this.line,this.col,t);this.addToken(Tr.HASH_VECTOR)}break;case";":for(;"\n"!=this.peek()&&!this.isAtEnd();)this.advance();break;case" ":case"\r":case"\t":break;case"\n":this.line++,this.col=0;break;case'"':this.stringToken();break;case"|":this.identifierTokenLoose();break;default:if(this.isDigit(t)||"-"===t||"+"===t||"."===t||"i"===t||"n"===t)this.identifierNumberToken();else{if(!this.isValidIdentifier(t))throw new ns(this.line,this.col,t);this.identifierToken()}}}comment(){for(;("|"!=this.peek()||"#"!=this.peekNext())&&!this.isAtEnd();)"\n"===this.peek()&&(this.line++,this.col=0),this.advance();if(this.isAtEnd())throw new rs(this.line,this.col);this.jump(),this.jump()}identifierToken(){for(;this.isValidIdentifier(this.peek());)this.advance();this.addToken(this.checkKeyword())}identifierTokenLoose(){for(this.advance();"|"!=this.peek()&&!this.isAtEnd();)"\n"===this.peek()&&(this.line++,this.col=0),this.advance();if(this.isAtEnd())throw new rs(this.line,this.col);this.advance(),this.addToken(this.checkKeyword())}identifierNumberToken(){for(;this.isValidIdentifier(this.peek());)this.advance();const t=this.source.substring(this.start,this.current);$r(t,Pr.COMPLEX).result?this.addToken(Tr.NUMBER,t):this.addToken(this.checkKeyword())}checkKeyword(){var t=this.source.substring(this.start,this.current);return ss.has(t)?ss.get(t):Tr.IDENTIFIER}stringToken(){for(;'"'!=this.peek()&&!this.isAtEnd();)"\n"===this.peek()&&(this.line++,this.col=0),this.advance();if(this.isAtEnd())throw new rs(this.line,this.col);this.advance();const t=this.source.substring(this.start+1,this.current-1);this.addToken(Tr.STRING,t)}booleanToken(){this.addToken(Tr.BOOLEAN,"t"===this.peekPrev())}match(t){return!this.isAtEnd()&&(this.source.charAt(this.current)==t&&(this.current++,!0))}peek(){return this.isAtEnd()?"\0":this.source.charAt(this.current)}peekNext(){return this.current+1>=this.source.length?"\0":this.source.charAt(this.current+1)}peekPrev(){return this.current-1<0?"\0":this.source.charAt(this.current-1)}isDigit(t){return t>="0"&&t<="9"}isSpecialSyntax(t){return"("===t||")"===t||"["===t||"]"===t||";"===t||"|"===t}isValidIdentifier(t){return!this.isWhitespace(t)&&!this.isSpecialSyntax(t)}isWhitespace(t){return" "===t||"\0"===t||"\n"===t||"\r"===t||"\t"===t}}var as,os;!function(t){class e{location;expressions;constructor(t,e){this.location=t,this.expressions=e}accept(t){return t.visitSequence(this)}equals(t){if(t instanceof e){if(this.expressions.length!==t.expressions.length)return!1;for(let e=0;e=this.tokens.length}previous(){return this.tokens[this.current-1]}peek(){return this.tokens[this.current]}validateChapter(t,e){if(this.chapter{}){if(0===t.length)return[[],void 0];if(1===t.length)return e(t[0]),[[this.parseExpression(t[0])],void 0];const n=t.at(-2);if(Wr(n)&&n.type===Tr.DOT){const n=t.at(-1),r=t.slice(0,-2);return e(n),r.forEach(e),[r.map(this.parseExpression.bind(this)),this.parseExpression(n)]}const r=t;return r.forEach(e),[r.map(this.parseExpression.bind(this)),void 0]}grouping(t){const e=[];let n=!1;t&&(n=!0,e.push(t));do{let t=this.advance();switch(t.type){case Tr.LEFT_PAREN:case Tr.LEFT_BRACKET:const r=this.grouping(t);e.push(r);break;case Tr.RIGHT_PAREN:case Tr.RIGHT_BRACKET:if(!n)throw new Xr(this.source,t.pos,t);e.push(t),n=!1;break;case Tr.APOSTROPHE:case Tr.BACKTICK:case Tr.COMMA:case Tr.COMMA_AT:case Tr.HASH_VECTOR:let s;do{s=this.grouping()}while(!s);e.push(this.affect(t,s));break;case Tr.QUOTE:case Tr.QUASIQUOTE:case Tr.UNQUOTE:case Tr.UNQUOTE_SPLICING:case Tr.IDENTIFIER:case Tr.NUMBER:case Tr.BOOLEAN:case Tr.STRING:case Tr.DOT:case Tr.DEFINE:case Tr.IF:case Tr.ELSE:case Tr.COND:case Tr.LAMBDA:case Tr.LET:case Tr.SET:case Tr.BEGIN:case Tr.DELAY:case Tr.IMPORT:case Tr.EXPORT:case Tr.DEFINE_SYNTAX:case Tr.SYNTAX_RULES:e.push(t);break;case Tr.HASH_SEMICOLON:for(;!this.grouping(););break;case Tr.EOF:throw new Gr(this.source,t.pos);default:throw new Xr(this.source,t.pos,t)}}while(n);if(0!==e.length)try{return jr.build(e)}catch(t){if(t instanceof Kr)throw new Kr(this.source,t.loc,t.form,t.expected);throw t}}affect(t,e){return jr.build([t,e])}parseExpression(t){return Wr(t)?this.parseToken(t):t.isSingleIdentifier()?this.parseToken(t.unwrap()[0]):this.parseGroup(t)}parseToken(t){switch(t.type){case Tr.IDENTIFIER:return this.quoteMode===cs.NONE?new as.Identifier(this.toLocation(t),t.lexeme):new as.Symbol(this.toLocation(t),t.lexeme);case Tr.NUMBER:return new as.NumericLiteral(this.toLocation(t),t.literal);case Tr.BOOLEAN:return new as.BooleanLiteral(this.toLocation(t),t.literal);case Tr.STRING:return new as.StringLiteral(this.toLocation(t),t.literal);default:if(this.quoteMode!==cs.NONE||this.chapter>=5)return new as.Symbol(this.toLocation(t),t.lexeme);throw new Xr(this.source,t.pos,t)}}parseGroup(t){if(!t.isParenthesized())return this.parseAffectorGroup(t);switch(this.quoteMode){case cs.NONE:return this.parseNormalGroup(t);case cs.QUOTE:case cs.QUASIQUOTE:return this.parseQuotedGroup(t)}}parseAffectorGroup(t){const[e,n]=t.unwrap();switch(e.type){case Tr.APOSTROPHE:case Tr.QUOTE:if(this.validateChapter(e,2),this.quoteMode!==cs.NONE){const t=this.parseExpression(n),r=new as.Symbol(this.toLocation(e),"quote"),s=r.location.merge(t.location);return new os.List(s,[r,t])}this.quoteMode=cs.QUOTE;const r=this.parseExpression(n);return this.quoteMode=cs.NONE,r;case Tr.BACKTICK:case Tr.QUASIQUOTE:if(this.validateChapter(e,2),this.quoteMode!==cs.NONE){const t=this.parseExpression(n),r=new as.Symbol(this.toLocation(e),"quasiquote"),s=r.location.merge(t.location);return new os.List(s,[r,t])}this.quoteMode=cs.QUASIQUOTE;const s=this.parseExpression(n);return this.quoteMode=cs.NONE,s;case Tr.COMMA:case Tr.UNQUOTE:this.validateChapter(e,2);let i=this.quoteMode;if(i===cs.NONE)throw new Zr(this.source,e.pos,e);if(i===cs.QUOTE){const t=this.parseExpression(n),r=new as.Symbol(this.toLocation(e),"unquote"),s=r.location.merge(t.location);return new os.List(s,[r,t])}this.quoteMode=cs.NONE;const a=this.parseExpression(n);return this.quoteMode=i,a;case Tr.COMMA_AT:case Tr.UNQUOTE_SPLICING:this.validateChapter(e,2);let o=this.quoteMode;if(o===cs.NONE)throw new Xr(this.source,e.pos,e);if(o===cs.QUOTE){const t=this.parseExpression(n),r=new as.Symbol(this.toLocation(e),"unquote-splicing"),s=r.location.merge(t.location);return new os.List(s,[r,t])}this.quoteMode=cs.NONE;const c=this.parseExpression(n);this.quoteMode=o;const u=this.toLocation(e).merge(c.location);return new as.SpliceMarker(u,c);case Tr.HASH_VECTOR:this.validateChapter(e,3);let h=this.quoteMode;this.quoteMode=cs.QUOTE;const l=this.parseVector(t);return this.quoteMode=h,l;default:throw new Xr(this.source,e.pos,e)}}parseNormalGroup(t){if(0===t.length()){if(this.chapter>=5)return new as.Nil(t.location);throw new Kr(this.source,t.location.start,t,"non-empty group")}const e=t.unwrap()[0];if(Wr(e))switch(e.type){case Tr.LAMBDA:return this.validateChapter(e,1),this.parseLambda(t);case Tr.DEFINE:return this.validateChapter(e,1),this.parseDefinition(t);case Tr.IF:return this.validateChapter(e,1),this.parseConditional(t);case Tr.LET:return this.validateChapter(e,1),this.parseLet(t);case Tr.COND:return this.validateChapter(e,1),this.parseExtendedCond(t);case Tr.QUOTE:case Tr.APOSTROPHE:case Tr.QUASIQUOTE:case Tr.BACKTICK:case Tr.UNQUOTE:case Tr.COMMA:case Tr.UNQUOTE_SPLICING:case Tr.COMMA_AT:return this.validateChapter(e,2),this.parseAffectorGroup(t);case Tr.BEGIN:return this.validateChapter(e,3),this.parseBegin(t);case Tr.DELAY:return this.validateChapter(e,3),this.parseDelay(t);case Tr.SET:return this.validateChapter(e,3),this.parseSet(t);case Tr.DEFINE_SYNTAX:return this.validateChapter(e,5),this.parseDefineSyntax(t);case Tr.SYNTAX_RULES:throw new Xr(this.source,e.pos,e);case Tr.IMPORT:return this.validateChapter(e,1),this.parseImport(t);case Tr.EXPORT:return this.validateChapter(e,1),this.parseExport(t);case Tr.VECTOR:return this.validateChapter(e,3),this.parseAffectorGroup(t);default:return this.parseApplication(t)}return this.parseApplication(t)}parseQuotedGroup(t){if(0===t.length())return new as.Nil(t.location);if(1===t.length()){const e=[this.parseExpression(t.unwrap()[0])];return new os.List(t.location,e)}const e=t.unwrap(),[n,r]=this.destructureList(e);return new os.List(t.location,n,r)}parseLambda(t){if(t.length()<3)throw new Kr(this.source,t.location.start,t,"(lambda (* . ?) +) | (lambda +)");const e=t.unwrap(),n=e[1],r=e.slice(2);let s,i=[];if(Wr(n)){if(n.type!==Tr.IDENTIFIER)throw new Kr(this.source,n.pos,n,"");s=new as.Identifier(this.toLocation(n),n.lexeme)}else{const t=n.unwrap();[i,s]=this.destructureList(t,(t=>{if(!Wr(t))throw new Kr(this.source,t.pos,t,"");if(t.type!==Tr.IDENTIFIER)throw new Kr(this.source,t.pos,t,"")}))}const a=r.map(this.parseExpression.bind(this));if(a.length<1)throw new Kr(this.source,t.location.start,t,"(lambda ... +)");if(1===a.length)return new as.Lambda(t.location,a[0],i,s);const o=a.at(0).location.merge(a.at(-1).location),c=new as.Sequence(o,a);return new as.Lambda(t.location,c,i,s)}parseDefinition(t){if(t.length()<3)throw new Kr(this.source,t.location.start,t,"(define ) | (define ( ) +)");const e=t.unwrap(),n=e[1],r=e.slice(2);let s,i,a=[],o=!1;if(Jr(n)){o=!0;const t=n.unwrap(),e=t[0],r=t.splice(1);if(!Wr(e))throw new Kr(this.source,e.location.start,e,"");if(e.type!==Tr.IDENTIFIER)throw new Kr(this.source,e.pos,e,"");s=new as.Identifier(this.toLocation(e),e.lexeme),[a,i]=this.destructureList(r,(t=>{if(!Wr(t))throw new Kr(this.source,t.pos,t,"");if(t.type!==Tr.IDENTIFIER)throw new Kr(this.source,t.pos,t,"")}))}else{if(n.type!==Tr.IDENTIFIER)throw new Kr(this.source,n.pos,n,"");s=new as.Identifier(this.toLocation(n),n.lexeme),o=!1}if(r.length<1)throw new Kr(this.source,t.location.start,t,"(define ... +)");if(o){const e=r.map(this.parseExpression.bind(this));if(1===e.length)return new os.FunctionDefinition(t.location,s,e[0],a,i);const n=e.at(0).location.merge(e.at(-1).location),o=new as.Sequence(n,e);return new os.FunctionDefinition(t.location,s,o,a,i)}if(r.length>1)throw new Kr(this.source,t.location.start,t,"(define )");const c=this.parseExpression(r[0]);return new as.Definition(t.location,s,c)}parseConditional(t){if(t.length()<3||t.length()>4)throw new Kr(this.source,t.location.start,t,"(if ?)");const e=t.unwrap(),n=e[1],r=e[2],s=t.length()>3?e[3]:void 0,i=this.parseExpression(n),a=this.parseExpression(r),o=s?this.parseExpression(s):new as.Identifier(t.location,"undefined");return new as.Conditional(t.location,i,a,o)}parseApplication(t){if(t.length()<1)throw new Kr(this.source,t.location.start,t,"( *)");const e=t.unwrap(),n=e[0],r=e.splice(1),s=this.parseExpression(n),i=[];for(const t of r)i.push(this.parseExpression(t));return new as.Application(t.location,s,i)}parseLet(t){if(this.chapter>=5){return t.unwrap().slice(1).forEach((t=>{this.parseExpression(t)})),new os.Let(t.location,[],[],new as.Identifier(t.location,"undefined"))}if(t.length()<3)throw new Kr(this.source,t.location.start,t,"(let (( )*) +)");const e=t.unwrap(),n=e[1],r=e.slice(2);if(!Jr(n))throw new Kr(this.source,n.pos,n,"(( )*)");const s=[],i=[],a=n.unwrap();for(const t of a){if(!Jr(t))throw new Kr(this.source,t.pos,t,"( )");if(2!==t.length())throw new Kr(this.source,t.location.start,t,"( )");const[e,n]=t.unwrap();if(!Wr(e))throw new Kr(this.source,e.location.start,e,"");if(e.type!==Tr.IDENTIFIER)throw new Kr(this.source,e.pos,e,"");s.push(new as.Identifier(this.toLocation(e),e.lexeme)),i.push(this.parseExpression(n))}const o=r.map(this.parseExpression.bind(this));if(o.length<1)throw new Kr(this.source,t.location.start,t,"(let ... +)");if(1===o.length)return new os.Let(t.location,s,i,o[0]);const c=o.at(0).location.merge(o.at(-1).location),u=new as.Sequence(c,o);return new os.Let(t.location,s,i,u)}parseExtendedCond(t){if(this.chapter>=5){return t.unwrap().slice(1).forEach((t=>{this.parseExpression(t)})),new os.Cond(t.location,[],[],new as.Identifier(t.location,"undefined"))}if(t.length()<2)throw new Kr(this.source,t.location.start,t,"(cond ( *)* (else )?)");const e=t.unwrap().splice(1),n=e.pop(),r=[],s=[];for(const t of e){if(!Jr(t))throw new Kr(this.source,t.pos,t,"( *)");if(t.length()<1)throw new Kr(this.source,t.firstToken().pos,t.firstToken(),"( *)");const[e,...n]=t.unwrap();if(Wr(e)&&e.type===Tr.ELSE)throw new Kr(this.source,e.pos,e,"");const i=this.parseExpression(e),a=n.map(this.parseExpression.bind(this)),o=n.length<1?i.location:a.at(0).location.merge(a.at(-1).location),c=n.length<1?i:n.length<2?a[0]:new as.Sequence(o,a);r.push(i),s.push(c)}if(!Jr(n))throw new Kr(this.source,n.pos,n,"( +) | (else )");if(n.length()<2)throw new Kr(this.source,n.firstToken().pos,n.firstToken(),"( +) | (else )");const[i,...a]=n.unwrap();let o=!1;if(Wr(i)&&i.type===Tr.ELSE&&(o=!0,1!==a.length))throw new Kr(this.source,n.location.start,n,"(else )");if(a.length<1)throw new Kr(this.source,n.location.start,n,"( +)");const c=a.map(this.parseExpression.bind(this)),u=c.at(0).location.merge(c.at(-1).location),h=1===a.length?c[0]:new as.Sequence(u,c);if(o)return new os.Cond(t.location,r,s,h);const l=this.parseExpression(i);return r.push(l),s.push(h),new os.Cond(t.location,r,s)}parseSet(t){if(3!==t.length())throw new Kr(this.source,t.location.start,t,"(set! )");const e=t.unwrap(),n=e[1],r=e[2];if(Jr(n))throw new Kr(this.source,n.location.start,n,"");if(n.type!==Tr.IDENTIFIER)throw new Kr(this.source,n.pos,n,"");const s=new as.Identifier(this.toLocation(n),n.lexeme),i=this.parseExpression(r);return new as.Reassignment(t.location,s,i)}parseBegin(t){if(t.length()<2)throw new Kr(this.source,t.location.start,t,"(begin +)");const e=t.unwrap().slice(1),n=[];for(const t of e)n.push(this.parseExpression(t));return new os.Begin(t.location,n)}parseDelay(t){if(this.chapter>=5){return t.unwrap().slice(1).forEach((t=>{this.parseExpression(t)})),new os.Delay(t.location,new as.Identifier(t.location,"undefined"))}if(2!==t.length())throw new Kr(this.source,t.location.start,t,"(delay )");const e=t.unwrap()[1],n=this.parseExpression(e);return new os.Delay(t.location,n)}parseDefineSyntax(t){if(3!==t.length())throw new Kr(this.source,t.location.start,t,"(define-syntax )");const e=t.unwrap(),n=e[1],r=e[2];this.quoteMode=cs.QUOTE;const s=this.parseExpression(n);if(this.quoteMode=cs.NONE,!(s instanceof as.Symbol))throw new Kr(this.source,s.location.start,n,"");if(!Jr(r))throw new Kr(this.source,r.pos,r,"");if(r.length()<2)throw new Kr(this.source,r.firstToken().pos,r,"(syntax-rules ...)");const i=r.unwrap()[0];if(!Wr(r.unwrap()[0]))throw new Kr(this.source,r.firstToken().pos,i,"syntax-rules");if(i.type!==Tr.SYNTAX_RULES)throw new Kr(this.source,i.pos,i,"syntax-rules");const a=this.parseSyntaxRules(r);return new as.DefineSyntax(t.location,s,a)}isValidPattern(t){if(t instanceof os.List){if(void 0===t.terminator){if(t.elements.filter((t=>t instanceof as.Symbol&&"..."===t.value)).length>1)return!1;const e=t.elements.findIndex((t=>t instanceof as.Symbol&&"..."===t.value));if(-1!=e&&0===e)return!1;for(const e of t.elements)if(!this.isValidPattern(e))return!1;return!0}{if(t.elements.filter((t=>t instanceof as.Symbol&&"..."===t.value)).length>1)return!1;const e=t.elements.findIndex((t=>t instanceof as.Symbol&&"..."===t.value));if(-1!=e){if(0===e)return!1;if(e===t.elements.length-1)return!1}for(const e of t.elements)if(!this.isValidPattern(e))return!1;return this.isValidPattern(t.terminator)}}return t instanceof as.Symbol||t instanceof as.BooleanLiteral||t instanceof as.NumericLiteral||t instanceof as.StringLiteral||t instanceof as.Nil}isValidTemplate(t){if(t instanceof os.List){if(void 0===t.terminator){if(0===t.elements.length)return!1;if(2===t.elements.length&&t.elements[0]instanceof as.Symbol&&"..."===t.elements[0].value)return this.isValidTemplate(t.elements[1]);let e=!1;for(let n=0;n*) +)");const e=t.unwrap(),n=e[1],r=e.slice(2),s=[];if(!Jr(n))throw new Kr(this.source,n.pos,n,"(*)");this.quoteMode=cs.QUOTE;for(const t of n.unwrap()){if(!Wr(t))throw new Kr(this.source,t.location.start,t,"");const e=this.parseExpression(t);if(!(e instanceof as.Symbol))throw new Kr(this.source,t.pos,t,"");s.push(e)}const i=[];for(const t of r){if(!Jr(t))throw new Kr(this.source,t.pos,t,"(