diff --git a/.env.example b/.env.example new file mode 100644 index 00000000..0a5d8b49 --- /dev/null +++ b/.env.example @@ -0,0 +1,3 @@ +# Google Gemini API Key for LLM TODO solver +# Get your API key from: https://ai.google.dev/gemini-api/docs/api-key +GOOGLE_API_KEY=your_google_api_key_here diff --git a/.gitignore b/.gitignore index 81ff4f9b..e3d81231 100644 --- a/.gitignore +++ b/.gitignore @@ -10,6 +10,9 @@ LICENSE yarn.lock package-lock.json +# Environment variables (contains API keys) +.env +.env.local compiled /doc diff --git a/LLM_SETUP.md b/LLM_SETUP.md new file mode 100644 index 00000000..92b876ed --- /dev/null +++ b/LLM_SETUP.md @@ -0,0 +1,44 @@ +# LLM TODO Solver Setup + +This project uses Google's Gemini API for LLM-powered TODO solving in Pie code. + +## Setup Instructions + +1. **Get a Google Gemini API Key** + - Visit: https://ai.google.dev/gemini-api/docs/api-key + - Sign in with your Google account + - Create a new API key + +2. **Configure the API Key** + - Copy `.env.example` to `.env`: + ```bash + cp .env.example .env + ``` + - Edit `.env` and replace `your_google_api_key_here` with your actual API key: + ``` + GOOGLE_API_KEY=your_actual_api_key_here + ``` + +3. **Run Tests** + ```bash + npm test -- test_llm.ts + ``` + +## Important Notes + +- **Never commit `.env` file to git** - it's already in `.gitignore` +- The `.env.example` file is safe to commit (it has no real key) +- If you get an error about missing API key, make sure `.env` file exists and contains your key + +## Free Tier Limits + +Google Gemini free tier has rate limits: +- 10 requests per minute +- If you hit the limit, tests will fail with quota errors +- Wait a minute and try again + +## Security + +- Keep your API key private +- Don't share it in commits, screenshots, or public channels +- If accidentally exposed, regenerate a new key immediately diff --git a/dist/index.js b/dist/index.js index 1fcb0e47..87e571f6 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,"(