From c39d1354c85c73d4ef4ec435aa4bee3a7ffbf3e4 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 11 Oct 2025 13:17:44 -0700 Subject: [PATCH] Primitive "Add missing cases" for vscode --- TODO.md | 49 ++++++++++++++++++++++-------------- bootstrap/newt.js | 24 ++++++++++-------- newt-vscode/src/extension.ts | 44 +++++++++++++++++++++++++++++++- src/Lib/Common.newt | 14 +++++++++-- src/Lib/Elab.newt | 22 ++++++++++++++-- src/Lib/Parser.newt | 23 +++++++++-------- 6 files changed, 131 insertions(+), 45 deletions(-) diff --git a/TODO.md b/TODO.md index 912e40d..5e90adb 100644 --- a/TODO.md +++ b/TODO.md @@ -1,6 +1,19 @@ ## TODO +- [ ] in-scope type at point in vscode + - So the idea here is that the references will be via FC, we remember the type at declaration and then point the usage back to the declaration (FC -> FC). We could dump all of this. (If we're still doing json.) + - Do we want to (maybe later) keep the scope as a FC? We could do scope at point then. + - But ideally we'd switch to a server/repl, so we don't have to mess around with serializing stuff. +- [ ] LSP and/or more editor support + - [ ] would be nice to have "add missing cases" and "case split" + - [x] Probably need ranges for FC + - [ ] leave an interactive process running + - [ ] collect metadata or run through the serialization data + - [ ] rename in editor for top level functions (and maybe stuff in scope probably need LSP first) +- [ ] Look into descriptions, etc. + - Can generating descriptions help with automatic "show" implementations + - We lost debug printing when switching to numeric tags - [ ] Add info to Ref/VRef (is dcon, arity, etc) - To save lookups during compilation and it might make eval faster - [x] number tags for data constructors @@ -14,7 +27,8 @@ - [ ] Maybe add qualified names to surface syntax and allow / detect conflicts on reference - [ ] Add `export` keywords - [ ] vscode - run newt when switching editors -- [ ] who calls X? We can only do this scoped to the current context for now. Someday whole source dir. +- [ ] who calls X? We can only do this scoped to the current context for now. Someday whole source dir. #lsp +- [ ] Magic to make Bool a boolean - [ ] case split - We could fake this up: - given a name and a point in the editor @@ -23,9 +37,9 @@ - enumerate valid constructors (and their arity) - Repeat the line with each, applied to args - For `<-` or `let` we'd want to fudge some `|` lines -- [ ] Support "Add missing cases" - - We could possibly fake up missing cases, too. Since they're listed and have an FC pointing at the first one - - [ ] Might need proper, enumerated errors for that +- [x] Support "Add missing cases" + - This has been hakced together + - We could possibly fake up missing cases, too. Since they're listed and have an FC pointing at the first one - [x] inline struct getters during code generation (We'd like `x.h1.h2`) - [ ] Better FC for parse errors (both EOF and the ones that show up just after the error) - [x] Code gen for PiType (rather than static JS) @@ -58,12 +72,7 @@ - [ ] see if we can make the typeclass stuff a little leaner, e.g. inline a projection of a static record. - It would be nice if IO looked like imperative JS, but that might be a bit of a stretch. -- [ ] LSP and/or more editor support - - [ ] would be nice to have "add missing cases" and "case split" - - [ ] Probably need ranges for FC - - [ ] leave an interactive process running - - [ ] collect metadata or run through the serialization data - - [ ] rename in editor for top level functions (and maybe stuff in scope, probably need LSP first) + - [ ] warn on unused imports? - [x] redo code to determine base path - [x] emit only one branch for default case when splitting inductives @@ -78,9 +87,10 @@ - [x] get port to run - [x] something goes terribly wrong with traverse_ and for_ (related to erasure, I think) - [x] ~~don't use `take` - it's not stack safe~~ The newt version is stack safe -- [ ] report info in case of error +- [ ] show user hole info even in case of error - [x] tokenizer that can be ported to newt - [ ] Add default path for library, so we don't need symlinks everywhere and can write tests for the library + - We need this to work for tests / dev and for installed newt. - [x] string interpolation? - The tricky part here is the `}` - I need to run the normal tokenizer in a way that treats `}` specially. - Idris handles `putStrLn "done \{ show $ add {x=1} 2}"` - it recurses for `{` `}` pairs. Do we want that complexity? @@ -91,7 +101,8 @@ - [x] for parse error, seek to col 0 token and process next decl - [x] record update sugar - [x] Change `Ord` to be more like Idris - LT / EQ / GT (and entail equality) -- [ ] Keep a `compare` function on `SortedMap` (like lean) +- [x] Keep a `compare` function on `SortedMap` (like lean) + - `emptyMap` helper defaults to `compare` from `Ord a` - [x] keymap for monaco - [x] SortedMap.newt issue in `where` - [x] fix "insufficient patterns", wire in M or Either String @@ -163,7 +174,7 @@ - [x] Check for shadowing when declaring dcon - Handles the forward decl in `Zoo1.newt`, but we'll need different syntax if we have different core terms for TCon/DCon/Function -- [ ] Require infix decl before declaring names with `_` (helps find bugs) or implicitly define infixl something if it's missing +- [ ] Require infix decl before declaring mixfix names with `_` (helps find bugs) or implicitly define as infixl something if it is missing - [x] sugar for typeclasses - [x] maybe add implicits in core to help resugar operators? - [ ] consider putting binders in environment, like Idris, to better mark `let` and to provide names @@ -182,7 +193,8 @@ - actual `if_then_else_` isn't practical because the language is strict - [x] Search should look at context - [ ] copattern matching -- [ ] Get `Combinatory.newt` to work +- [x] Get `Combinatory.newt` to work + - Fixed when eval was fixed - [x] Remember operators from imports - [x] Default cases for non-primitives (currently gets expanded to all constructors) - This may need a little care. But I think I could collect all constructors that only match wildcards into a single case. This would lose any information from breaking out the individual, unnamed cases though. @@ -235,11 +247,9 @@ - [x] push down to value/term - [x] check quantity - [x] erase in output - - [ ] remove erased top level arguments +- [ ] remove erased top level arguments - [x] top level at point in vscode -- [ ] in-scope type at point in vscode - [ ] repl -- [ ] LSP - [x] don't match forced constructors at runtime - I think we got this by not switching for single cases - [x] magic nat (codegen as number with appropriate pattern matching) @@ -249,10 +259,11 @@ - [ ] add `pop` or variant of `pfunc` that maps to an operator, giving the js operator and precedence on RHS - This has now been hard-coded in codegen, but a syntax or something would be better. - [ ] consider moving caselet, etc. desugaring out of the parser -- [ ] pattern matching lambda +- [-] pattern matching lambda + - `\case` is sufficient - I kept wanting this in AoC and use it a lot in the newt code - This conflicts with current code (unused?) that allows telescope information in lambdas - - For now, I'll implement `\case` + ### Parsing diff --git a/bootstrap/newt.js b/bootstrap/newt.js index 90685d4..4f7936d 100644 --- a/bootstrap/newt.js +++ b/bootstrap/newt.js @@ -524,7 +524,7 @@ const Prelude_arrayToList = (a,arr) => { }; const Prelude_lines = (s) => Prelude_arrayToList(null,s.split('\n')); const Lib_Common_showError_go$27 = ( _, _1, _2, _3, _4, _$$5, _$$6 ) => (bouncer(Lib_Common_REC_showError_go$27, { tag: 1, h0: _, h1: _1, h2: _2, h3: _3, h4: _4, h5: _$$5, h6: _$$6 })); -const Lib_Common_REC_showError_go$27 = ( arg ) => { switch (arg.h6.tag) { case 1: { const sc$$10 = Prelude_jsEq(null, arg.h5, arg.h2.h1.h0); switch (sc$$10) { case 1: { const sc$$11 = Prelude_Prelude_Eq$20Prelude_Ordering$2C_$3D$3D_(Prelude_jsCompare(null, (arg.h2.h1.h0) - (3), arg.h5), 0); switch (sc$$11) { case 1: return { tag: 1, h0: arg.h0, h1: arg.h1, h2: arg.h2, h3: arg.h3, h4: arg.h4, h5: (arg.h5) + (1), h6: arg.h6.h2 }; case 0: return { tag: 0, h0: (" ") + ((arg.h6.h1) + (("\n") + (Lib_Common_showError_go$27(arg.h0, arg.h1, arg.h2, arg.h3, arg.h4, (arg.h5) + (1), arg.h6.h2)))) }; } break; } case 0: return { tag: 0, h0: ((((" ") + (arg.h6.h1)) + ("\n ")) + (Prelude_replicate(Prelude_intToNat(arg.h2.h1.h1), " "))) + ("^\n") }; } break; } case 0: return { tag: 0, h0: "" }; } }; +const Lib_Common_REC_showError_go$27 = ( arg ) => { switch (arg.h6.tag) { case 1: { const sc$$10 = Prelude_jsEq(null, arg.h5, arg.h2.h1.h0); switch (sc$$10) { case 1: { const sc$$11 = Prelude_Prelude_Eq$20Prelude_Ordering$2C_$3D$3D_(Prelude_jsCompare(null, (arg.h2.h1.h0) - (3), arg.h5), 0); switch (sc$$11) { case 1: return { tag: 1, h0: arg.h0, h1: arg.h1, h2: arg.h2, h3: arg.h3, h4: arg.h4, h5: (arg.h5) + (1), h6: arg.h6.h2 }; case 0: return { tag: 0, h0: (" ") + ((arg.h6.h1) + (("\n") + (Lib_Common_showError_go$27(arg.h0, arg.h1, arg.h2, arg.h3, arg.h4, (arg.h5) + (1), arg.h6.h2)))) }; } break; } case 0: { const width = ((arg.h2.h1.h3) - (arg.h2.h1.h1)) + (1); return { tag: 0, h0: ((((((" ") + (arg.h6.h1)) + ("\n ")) + (Prelude_replicate(Prelude_intToNat(arg.h2.h1.h1), " "))) + ("")) + (Prelude_replicate(Prelude_intToNat(width), "^"))) + ("\n") }; break; } } break; } case 0: return { tag: 0, h0: "" }; } }; const Lib_Common_showError_go = ( _, _1, _2, _3, _4, _5, _$$6, _$$7 ) => (bouncer(Lib_Common_REC_showError_go, { tag: 1, h0: _, h1: _1, h2: _2, h3: _3, h4: _4, h5: _5, h6: _$$6, h7: _$$7 })); const Lib_Common_REC_showError_go = ( arg ) => { switch (arg.h7.tag) { case 1: { const sc$$11 = Prelude_jsEq(null, arg.h6, arg.h2.h1.h0); switch (sc$$11) { case 1: { const sc$$12 = Prelude_Prelude_Eq$20Prelude_Ordering$2C_$3D$3D_(Prelude_jsCompare(null, (arg.h2.h1.h0) - (3), arg.h6), 0); switch (sc$$12) { case 1: return { tag: 1, h0: arg.h0, h1: arg.h1, h2: arg.h2, h3: arg.h3, h4: arg.h4, h5: arg.h5, h6: (arg.h6) + (1), h7: arg.h7.h2 }; case 0: return { tag: 0, h0: (" ") + ((arg.h7.h1) + (("\n") + (Lib_Common_showError_go(arg.h0, arg.h1, arg.h2, arg.h3, arg.h4, arg.h5, (arg.h6) + (1), arg.h7.h2)))) }; } break; } case 0: return { tag: 0, h0: ((((" ") + (arg.h7.h1)) + ("\n ")) + (Prelude_replicate(Prelude_intToNat(arg.h2.h1.h1), " "))) + ("^\n") }; } break; } case 0: return { tag: 0, h0: "" }; } }; const Main_processModule = ( _$$0, _$$1, _$$2, _$$3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const modns = Prelude_Prelude_Concat$20$28Prelude_List$20BND$3A0$29$2C_$2B$2B_(null, _$$3.h0, Prelude__$3A$3A_(null, _$$3.h1, Prelude_Nil(null))); const name = Prelude_joinBy(".", modns); const sc$$10 = Data_SortedMap_lookupMap(null, null, modns, top.h0); switch (sc$$10.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( tc ) => (Lib_Types_putTop(Lib_Types_MkTop(Data_SortedMap_updateMap(null, null, modns, Lib_Types_emptyModCtx(""), top.h0), tc.h1, tc.h2, tc.h3, tc.h4, tc.h5, tc.h6, tc.h7, tc.h8)))), ( _ ) => { const fn = (Prelude_joinBy("/", Prelude__$3A$3A_(null, _$$1, _$$3.h0))) + (("/") + ((_$$3.h1) + (".newt"))); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_HasIO$20Lib_Types_M$2CliftIO(null, Node_readFile(fn)), ( $$sc ) => { switch ($$sc.tag) { case 1: { const sc$$19 = Lib_Tokenizer_tokenise(fn, $$sc.h2); switch (sc$$19.tag) { case 1: { const sc$$23 = Lib_Parser_Impl_partialParse(null, fn, Lib_Parser_parseModHeader, top.h8, sc$$19.h2); switch (sc$$23.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _1 ) => ((("scan imports for module ") + (sc$$23.h2.h2.h3)) + (""))), ( _1 ) => { const ns = Prelude_split(sc$$23.h2.h2.h3, "."); const sc$$41 = Data_List1_unsnoc(null, Data_List1_split1(sc$$23.h2.h2.h3, ".")); const sc$$46 = Lib_Common_Prelude_Eq$20Lib_Common_QName$2C_$3D$3D_(_$$3, Lib_Common_QN(sc$$41.h2, sc$$41.h3)); switch (sc$$46) { case 0: { const sc$$47 = Lib_Parser_Impl_partialParse(null, fn, Lib_Parser_parseImports, sc$$23.h2.h3.h2, sc$$23.h2.h3.h3); switch (sc$$47.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, sc$$47.h2.h2, ( $$case ) => { const sc$$63 = Data_List1_unsnoc(null, Data_List1_split1($$case.h1, ".")); const qname = Lib_Common_QN(sc$$63.h2, sc$$63.h3); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_when(null, Lib_Types_Prelude_Applicative$20Lib_Types_M, Prelude_elem(null, Prelude_Prelude_Eq$20Prim_String, $$case.h1, _$$2), ( _2 ) => (Lib_Types_MkM(null, ( _3 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Common_emptyFC, (((("import loop ") + (name)) + (" -> ")) + ($$case.h1)) + (""))), eta)))))), ( _2 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Main_processModule($$case.h0, _$$1, Prelude__$3A$3A_(null, name, _$$2), qname), ( _3 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Prelude_split($$case.h1, ".")))))); }), ( imported ) => { const imported1 = Prelude_Prelude_Concat$20$28Prelude_List$20BND$3A0$29$2C_$2B$2B_(null, imported, Prelude__$3A$3A_(null, Lib_Common_primNS, Prelude_Nil(null))); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_HasIO$20Lib_Types_M$2CliftIO(null, Serialize_checksum($$sc.h2)), ( srcSum ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Main_moduleHash(srcSum, imported1), ( csum ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_HasIO$20Lib_Types_M$2CliftIO(null, Prelude_primPutStrLn((("module ") + (sc$$23.h2.h2.h3)) + (""))), ( _2 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top1 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Serialize_loadModule(_$$3, csum), ( $$sc1 ) => { switch ($$sc1.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _3 ) => (("MODNS ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Prelude_Prelude_Show$20Prim_String$2Cshow, modns))))), ( _3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top2 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Main_parseDecls(fn, top2.h8, sc$$47.h2.h3.h3, Prelude_Lin(null)), ( $$sc2 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top3 ) => { const freshMC = Lib_Types_MC(Data_SortedMap_EmptyMap(null, null, ( eta ) => (( eta1 ) => (Lib_Common_Prelude_Ord$20Lib_Common_QName$2Ccompare(eta, eta1)))), Prelude_Nil(null), 0, 0); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( tc ) => (Lib_Types_putTop(Lib_Types_MkTop(tc.h0, imported1, Data_SortedMap_EmptyMap(null, null, ( eta ) => (( eta1 ) => (Lib_Common_Prelude_Ord$20Lib_Common_QName$2Ccompare(eta, eta1)))), modns, Data_SortedMap_EmptyMap(null, null, ( eta ) => (( eta1 ) => (Lib_Common_Prelude_Ord$20Lib_Common_QName$2Ccompare(eta, eta1)))), freshMC, tc.h6, tc.h7, $$sc2.h3)))), ( _4 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, imported1, ( ns1 ) => { const sc$$80 = Data_SortedMap_lookupMap$27(null, null, ns1, top3.h0); switch (sc$$80.tag) { case 0: return Main_importHints(Data_SortedMap_listValues(null, null, sc$$80.h1.h1)); default: return Lib_Types_MkM(null, ( _5 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Common_emptyFC, (("namespace ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Prelude_Prelude_Show$20Prim_String$2Cshow, ns1)))) + (" missing"))), eta)))); } }), ( _5 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _6 ) => ("process Decls")), ( _6 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_Prelude_Traversable$20Prelude_List$2Ctraverse(null, null, null, Lib_Types_Prelude_Applicative$20Lib_Types_M, ( eta ) => (Main_processModule_tryProcessDecl(_$$0, _$$1, _$$2, _$$3, _$$3.h0, _$$3.h1, null, $$sc.h2, ns, eta)), Lib_Elab_collectDecl($$sc2.h2)), ( _7 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top4 ) => { const mod = Lib_Types_MkModCtx(csum, top4.h4, top4.h5, top4.h8); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_HasIO$20Lib_Types_M$2CliftIO(null, Data_IORef_primReadIORef(null, top4.h7)), ( errors ) => { const sc$$85 = Prelude__$26$26_(Prelude_not(Prelude_Prelude_Eq$20$28Prelude_List$20BND$3A1$29$2C_$3D$3D_(null, Prelude_Prelude_Eq$20Prim_String, _$$2, Prelude_Nil(null))), Prelude_jsEq(null, Prelude_length$27(null, errors), 0)); switch (sc$$85) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, 0), ( _8 ) => { const modules = Data_SortedMap_updateMap(null, null, modns, mod, top4.h0); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( tc ) => (Lib_Types_putTop(Lib_Types_MkTop(modules, tc.h1, tc.h2, tc.h3, tc.h4, tc.h5, tc.h6, tc.h7, tc.h8)))), ( _9 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_HasIO$20Lib_Types_M$2CliftIO(null, Data_IORef_primReadIORef(null, top4.h7)), ( $$sc3 ) => { switch ($$sc3.tag) { case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_ProcessDecl_logMetas(Prelude_reverse(null)(Data_SortedMap_listValues(null, null, top4.h5.h0))), ( _10 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, $$sc.h2))); default: return Node_exitFailure(null, "Compile failed"); } }))); }); case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Serialize_dumpModule(_$$3, $$sc.h2, mod), ( _8 ) => { const modules = Data_SortedMap_updateMap(null, null, modns, mod, top4.h0); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( tc ) => (Lib_Types_putTop(Lib_Types_MkTop(modules, tc.h1, tc.h2, tc.h3, tc.h4, tc.h5, tc.h6, tc.h7, tc.h8)))), ( _9 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_HasIO$20Lib_Types_M$2CliftIO(null, Data_IORef_primReadIORef(null, top4.h7)), ( $$sc3 ) => { switch ($$sc3.tag) { case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_ProcessDecl_logMetas(Prelude_reverse(null)(Data_SortedMap_listValues(null, null, top4.h5.h0))), ( _10 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, $$sc.h2))); default: return Node_exitFailure(null, "Compile failed"); } }))); }); } }); }))))))))); }))))))); case 0: { const modules = Data_SortedMap_updateMap(null, null, modns, $$sc1.h1, top1.h0); const ops = Data_SortedMap_foldMap(null, null, ( _$$21 ) => (( _$$31 ) => (_$$21)), top1.h8, Data_SortedMap_toList(null, null, $$sc1.h1.h3)); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( tc ) => (Lib_Types_putTop(Lib_Types_MkTop(modules, tc.h1, tc.h2, tc.h3, tc.h4, tc.h5, tc.h6, tc.h7, ops)))), ( _3 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, $$sc.h2))); break; } } }))))))))); }); case 0: return Node_exitFailure(null, Lib_Common_showError($$sc.h2, sc$$47.h2.h2)); } break; } default: return Node_exitFailure(null, (((((("ERROR at ") + (Lib_Common_Prelude_Show$20Lib_Common_FC$2Cshow(sc$$23.h2.h2.h2))) + (": module name ")) + (sc$$23.h2.h2.h3)) + (" doesn't match file name ")) + (fn)) + ("")); } }); case 0: return Node_exitFailure(null, Lib_Common_showError($$sc.h2, sc$$23.h2.h2)); } break; } case 0: return Node_exitFailure(null, Lib_Common_showError($$sc.h2, sc$$19.h2)); } break; } case 0: return Node_exitFailure(null, (((((("ERROR at ") + (Lib_Common_Prelude_Show$20Lib_Common_FC$2Cshow(_$$0))) + (": error reading ")) + (fn)) + (": ")) + ($$sc.h2)) + ("")); } }); }); default: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, ""); } })); @@ -641,8 +641,11 @@ const Prelude_Prelude_Show$20Prim_String = Prelude_MkShow(null, Prelude_Prelude_ const Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Pattern$2CgetFC = ( _$$0 ) => { switch (_$$0.tag) { case 3: return _$$0.h0; case 2: return _$$0.h0; case 1: return _$$0.h0; case 0: return _$$0.h0; } }; const Lib_Elab_checkDone_rename = ( _, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _$$15 ) => { switch (_$$15.tag) { case 1: { const sc$$23 = Prelude_jsEq(null, _$$15.h1.h2, _9); switch (sc$$23) { case 1: return Prelude__$3A$3A_(null, Prelude__$2C_(null, null, _$$15.h1.h2, _$$15.h1.h3), Lib_Elab_checkDone_rename(_, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _$$15.h2)); case 0: return Prelude__$3A$3A_(null, Prelude__$2C_(null, null, _13, _$$15.h1.h3), _$$15.h2); } break; } case 0: return Prelude_Nil(null); } }; const Lib_Syntax_Prelude_Show$20Lib_Syntax_Pattern = Prelude_MkShow(null, Lib_Syntax_Prelude_Show$20Lib_Syntax_Pattern$2Cshow); -const Lib_Elab_buildDefault = ( _$$0, _$$1, _$$2, _$$3, _$$4 ) => { const defclauses = Prelude_filter(null, ( eta ) => (Lib_Elab_buildDefault_isDefault(_$$0, _$$1, _$$2, _$$3, _$$4, null, eta)), _$$1.h0); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_when(null, Lib_Types_Prelude_Applicative$20Lib_Types_M, Prelude_jsEq(null, Prelude_length$27(null, defclauses), 0), ( _ ) => (Lib_Types_MkM(null, ( _1 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$2, (((("missing cases ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow, _$$4)))) + (" on ")) + (_$$3)) + (""))), eta)))))), ( _ ) => (Lib_Types_Prelude_Functor$20Lib_Types_M$2Cmap(null, null, Lib_Types_CaseDefault, Lib_Elab_buildTree(_$$0, Lib_Elab_MkProb(defclauses, _$$1.h1))))); }; -const Lib_Elab_buildDefault_isDefault = ( _, _1, _2, _3, _4, _5, _$$6 ) => { const sc$$7 = Prelude_find(null, ( _$$5 ) => (Prelude_jsEq(null, _3, _$$5.h2)), _$$6.h1); switch (sc$$7.tag) { case 1: return 0; case 0: switch (sc$$7.h1.h3.tag) { case 2: return 0; case 0: return 0; default: return 1; } break; } }; +const Lib_Elab_buildDefault = ( _$$0, _$$1, _$$2, _$$3, _$$4 ) => { const defclauses = Prelude_filter(null, ( eta ) => (Lib_Elab_buildDefault_applied_isDefault(_$$0, _$$1, _$$2, _$$3, _$$4, null, null, eta)), _$$1.h0); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_when(null, Lib_Types_Prelude_Applicative$20Lib_Types_M, Prelude_jsEq(null, Prelude_length$27(null, defclauses), 0), ( _ ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_Prelude_Traversable$20Prelude_List$2Ctraverse(null, null, null, Lib_Types_Prelude_Applicative$20Lib_Types_M, ( eta ) => (Lib_Elab_buildDefault_applied(_$$0, _$$1, _$$2, _$$3, _$$4, null, eta)), _$$4), ( missing ) => (Lib_Types_MkM(null, ( _1 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$2, (("missing cases: ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Prelude_Prelude_Show$20Prim_String$2Cshow, missing)))) + (""))), eta)))))))), ( _ ) => (Lib_Types_Prelude_Functor$20Lib_Types_M$2Cmap(null, null, Lib_Types_CaseDefault, Lib_Elab_buildTree(_$$0, Lib_Elab_MkProb(defclauses, _$$1.h1))))); }; +const Lib_Elab_buildDefault_applied = ( _, _1, _2, _3, _4, _5, _$$6 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$9 = Lib_TopContext_lookup(_$$6, top); switch (sc$$9.tag) { case 0: switch (sc$$9.h1.h3.tag) { case 2: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Elab_buildDefault_applied_go(_, _1, _2, _3, _4, _5, _$$6, null, _$$6.h1, sc$$9.h1.h2)); default: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, _$$6.h1); } break; default: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, _$$6.h1); } })); +const Lib_Elab_buildDefault_applied_go = ( _, _1, _2, _3, _4, _5, _6, _7, _$$8, _$$9 ) => (bouncer(Lib_Elab_REC_buildDefault_applied_go, { tag: 1, h0: _, h1: _1, h2: _2, h3: _3, h4: _4, h5: _5, h6: _6, h7: _7, h8: _$$8, h9: _$$9 })); +const Lib_Elab_REC_buildDefault_applied_go = ( arg ) => { switch (arg.h9.tag) { case 6: switch (arg.h9.h2) { case 1: return { tag: 1, h0: arg.h0, h1: arg.h1, h2: arg.h2, h3: arg.h3, h4: arg.h4, h5: arg.h5, h6: arg.h6, h7: arg.h7, h8: (("") + (arg.h8)) + (" _"), h9: arg.h9.h5 }; default: return { tag: 1, h0: arg.h0, h1: arg.h1, h2: arg.h2, h3: arg.h3, h4: arg.h4, h5: arg.h5, h6: arg.h6, h7: arg.h7, h8: arg.h8, h9: arg.h9.h5 }; } break; default: return { tag: 0, h0: arg.h8 }; } }; +const Lib_Elab_buildDefault_applied_isDefault = ( _, _1, _2, _3, _4, _5, _6, _$$7 ) => { const sc$$8 = Prelude_find(null, ( _$$5 ) => (Prelude_jsEq(null, _3, _$$5.h2)), _$$7.h1); switch (sc$$8.tag) { case 1: return 0; case 0: switch (sc$$8.h1.h3.tag) { case 2: return 0; case 0: return 0; default: return 1; } break; } }; const Lib_Types_Prelude_Show$20Lib_Types_CaseAlt$2Cshow = Lib_Types_showCaseAlt; const Lib_Types_Prelude_Show$20Lib_Types_CaseAlt = Prelude_MkShow(null, Lib_Types_Prelude_Show$20Lib_Types_CaseAlt$2Cshow); const Lib_Elab_buildCase = ( _$$0, _$$1, _$$2, _$$3, _$$4 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _ ) => ((((((("CASE ") + (_$$2)) + (" match ")) + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" ty ")) + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( _$$21 ) => (_$$21.h2), _$$0.h2), _$$4.h3.h3))), Prelude_Lin(null)))) + (""))), ( _ ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude_Nil(null), _$$4.h3.h3), ( vty ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_extendPi(_$$0, vty, Prelude_Lin(null), Prelude_Lin(null)), ( $$sc ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _1 ) => ((((("unify dcon cod with scrut\n ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow($$sc.h3.h2))) + ("\n ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$3))) + (""))), ( _1 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_catchError(null, Lib_Types_Prelude_Functor$20Lib_Types_M$2Cmap(null, null, ( eta ) => (Prelude_Just(null, eta)), Lib_Elab_unify($$sc.h2.h1, 1, $$sc.h3.h2, _$$3)), ( err ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _2 ) => ((((("SKIP ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" because unify error ")) + (Lib_Types_errorMsg(err))) + (""))), ( _2 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Prelude_Nothing(null)))))), ( $$sc1 ) => { switch ($$sc1.tag) { case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _2 ) => ((((("scrut ") + (_$$2)) + (" constrained to ")) + (Prelude_Prelude_Show$20$28Prelude_Maybe$20BND$3A1$29$2Cshow(null, Lib_Types_Prelude_Show$20Lib_Types_Val, Lib_Elab_lookupDef(_$$0, _$$2)))) + (""))), ( _2 ) => { switch (_$$3.tag) { case 1: { const sc$$44 = Lib_Elab_lookupDef(_$$0, _$$2); switch (sc$$44.tag) { case 0: switch (sc$$44.h1.tag) { case 1: { const sc$$50 = Prelude_not(Lib_Common_Prelude_Eq$20Lib_Common_QName$2C_$3D$3D_(sc$$44.h1.h1, _$$4.h2)); switch (sc$$50) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _3 ) => ((((("case ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" dotted ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(sc$$44.h1))) + (""))), ( _3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_when(null, Lib_Types_Prelude_Applicative$20Lib_Types_M, Prelude_not(Prelude_Prelude_Eq$20Prelude_Nat$2C_$3D$3D_(Prelude_length(null, $$sc.h3.h3.h2), Data_SnocList_snoclen(null, sc$$44.h1.h2))), ( _4 ) => (Lib_Types_MkM(null, ( _5 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Common_emptyFC, (((("") + (Prelude_showInt(Prelude_natToInt(Prelude_length(null, $$sc.h3.h3.h2))))) + (" vars /= ")) + (Prelude_showInt(Prelude_natToInt(Data_SnocList_snoclen(null, sc$$44.h1.h2))))) + (""))), eta)))))), ( _4 ) => { const lvl = (Prelude_length$27(null, $$sc.h2.h1)) - (Prelude_length$27(null, $$sc.h3.h3.h2)); const scons = Lib_Elab_buildCase_constrainSpine(_$$0, _$$1, _$$2, _$$3, _$$4, _$$4.h0, _$$4.h1, _$$4.h2, _$$4.h3, _$$4.h3.h0, _$$4.h3.h1, _$$4.h3.h2, _$$4.h3.h3, null, lvl, Prelude__$3C$3E$3E_(null, sc$$44.h1.h2, Prelude_Nil(null))); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_updateContext($$sc.h2, scons), ( ctx$27 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _5 ) => ((((((("(dcon ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" ty ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow($$sc.h3.h2))) + (" scty ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$3))) + (""))), ( _5 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _6 ) => ((((("(dcon ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (") (vars ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Elab_Prelude_Show$20Lib_Elab_Bind$2Cshow, $$sc.h3.h3.h2)))) + (") clauses were"))), ( _6 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, _$$1.h0, ( x ) => (Lib_Types_log(2, ( _7 ) => (((" ") + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Clause$2Cshow(x))) + (""))))), ( _7 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Functor$20Lib_Types_M$2Cmap(null, null, ( eta ) => (Prelude_mapMaybe(null, null, ( _$$11 ) => (_$$11), eta)), Prelude_Prelude_Traversable$20Prelude_List$2Ctraverse(null, null, null, Lib_Types_Prelude_Applicative$20Lib_Types_M, ( eta ) => (Lib_Elab_buildCase_constrainSpine_getName_makeConstr_rewriteConstraint_rewriteClause(_$$0, _$$1, _$$2, _$$3, _$$4, _$$4.h0, _$$4.h1, _$$4.h2, _$$4.h3, _$$4.h3.h0, _$$4.h3.h1, _$$4.h3.h2, _$$4.h3.h3, null, null, null, null, null, _$$3.h1, $$sc.h3.h3.h2, eta)), _$$1.h0)), ( clauses ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _8 ) => ("and now:")), ( _8 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, clauses, ( x ) => (Lib_Types_log(2, ( _9 ) => (((" ") + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Clause$2Cshow(x))) + (""))))), ( _9 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_when(null, Lib_Types_Prelude_Applicative$20Lib_Types_M, Prelude_jsEq(null, Prelude_length$27(null, clauses), 0), ( _10 ) => (Lib_Types_MkM(null, ( _11 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$0.h4, (((("Missing case for ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" splitting ")) + (_$$2)) + (""))), eta)))))), ( _10 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_buildTree(ctx$27, Lib_Elab_MkProb(clauses, _$$1.h1)), ( tm ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Prelude_Just(null, Lib_Types_CaseCons(_$$4.h2, Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( eta ) => (Lib_Elab_buildCase_constrainSpine_getName(_$$0, _$$1, _$$2, _$$3, _$$4, _$$4.h0, _$$4.h1, _$$4.h2, _$$4.h3, _$$4.h3.h0, _$$4.h3.h1, _$$4.h3.h2, _$$4.h3.h3, null, null, eta)), $$sc.h3.h3.h2), tm))))))))))))))))))))); }))); case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _3 ) => ((((((("SKIP ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" because ")) + (_$$2)) + (" forced to ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(sc$$44.h1))) + (""))), ( _3 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Prelude_Nothing(null)))); } break; } default: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_tryError(null, Lib_Elab_unify($$sc.h2.h1, 1, $$sc.h3.h2, _$$3)), ( $$sc2 ) => { switch ($$sc2.tag) { case 1: { const sc$$52 = Prelude_findIndex$27(null, ( _$$5 ) => (Prelude_jsEq(null, _$$2, _$$5.h2)), $$sc.h2.h2); switch (sc$$52.tag) { case 1: return Lib_Types_MkM(null, ( _3 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$0.h4, (("") + (_$$2)) + (" not is scope?"))), eta)))); case 0: { const lvl = ((Prelude_length$27(null, $$sc.h2.h1)) - (sc$$52.h1)) - (1); const scon = Prelude__$2C_(null, null, lvl, Lib_Types_VRef(_$$0.h4, _$$4.h2, $$sc.h3.h3.h3)); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _3 ) => ((("scty ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$3))) + (""))), ( _3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _4 ) => ((("UNIFY results ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( eta ) => (Prelude_Prelude_Show$20$28Prelude__$D7_$20BND$3A3$20BND$3A2$29$2Cshow(null, null, Prelude_Prelude_Show$20Prim_Int, Lib_Types_Prelude_Show$20Lib_Types_Val, eta)), $$sc2.h2.h0)))) + (""))), ( _4 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _5 ) => ((("before types: ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( eta ) => (Prelude_Prelude_Show$20$28Prelude__$D7_$20BND$3A3$20BND$3A2$29$2Cshow(null, null, Prelude_Prelude_Show$20Prim_String, Lib_Types_Prelude_Show$20Lib_Types_Val, eta)), $$sc.h2.h2)))) + (""))), ( _5 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _6 ) => ((("before env: ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, $$sc.h2.h1)))) + (""))), ( _6 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _7 ) => ((("SC CONSTRAINT: ") + (Prelude_Prelude_Show$20$28Prelude__$D7_$20BND$3A3$20BND$3A2$29$2Cshow(null, null, Prelude_Prelude_Show$20Prim_Int, Lib_Types_Prelude_Show$20Lib_Types_Val, scon))) + (""))), ( _7 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_updateContext($$sc.h2, Prelude__$3A$3A_(null, scon, $$sc2.h2.h0)), ( ctx$27 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _8 ) => ((("context types: ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( eta ) => (Prelude_Prelude_Show$20$28Prelude__$D7_$20BND$3A3$20BND$3A2$29$2Cshow(null, null, Prelude_Prelude_Show$20Prim_String, Lib_Types_Prelude_Show$20Lib_Types_Val, eta)), ctx$27.h2)))) + (""))), ( _8 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _9 ) => ((("context env: ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, ctx$27.h1)))) + (""))), ( _9 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _10 ) => ((((((("(dcon ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" ty ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow($$sc.h3.h2))) + (" scty ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$3))) + (""))), ( _10 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _11 ) => ((((("(dcon ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (") (vars ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Elab_Prelude_Show$20Lib_Elab_Bind$2Cshow, $$sc.h3.h3.h2)))) + (") clauses were"))), ( _11 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, _$$1.h0, ( x ) => (Lib_Types_log(2, ( _12 ) => (((" ") + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Clause$2Cshow(x))) + (""))))), ( _12 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Functor$20Lib_Types_M$2Cmap(null, null, ( eta ) => (Prelude_mapMaybe(null, null, ( _$$11 ) => (_$$11), eta)), Prelude_Prelude_Traversable$20Prelude_List$2Ctraverse(null, null, null, Lib_Types_Prelude_Applicative$20Lib_Types_M, ( eta ) => (Lib_Elab_buildCase_constrainSpine_getName_makeConstr_rewriteConstraint_rewriteClause(_$$0, _$$1, _$$2, _$$3, _$$4, _$$4.h0, _$$4.h1, _$$4.h2, _$$4.h3, _$$4.h3.h0, _$$4.h3.h1, _$$4.h3.h2, _$$4.h3.h3, null, null, null, null, null, _$$3.h1, $$sc.h3.h3.h2, eta)), _$$1.h0)), ( clauses ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _13 ) => ("and now:")), ( _13 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, clauses, ( x ) => (Lib_Types_log(2, ( _14 ) => (((" ") + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Clause$2Cshow(x))) + (""))))), ( _14 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_when(null, Lib_Types_Prelude_Applicative$20Lib_Types_M, Prelude_jsEq(null, Prelude_length$27(null, clauses), 0), ( _15 ) => (Lib_Types_MkM(null, ( _16 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$0.h4, (((("Missing case for ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" splitting ")) + (_$$2)) + (""))), eta)))))), ( _15 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_buildTree(ctx$27, Lib_Elab_MkProb(clauses, _$$1.h1)), ( tm ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Prelude_Just(null, Lib_Types_CaseCons(_$$4.h2, Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( eta ) => (Lib_Elab_buildCase_constrainSpine_getName(_$$0, _$$1, _$$2, _$$3, _$$4, _$$4.h0, _$$4.h1, _$$4.h2, _$$4.h3, _$$4.h3.h0, _$$4.h3.h1, _$$4.h3.h2, _$$4.h3.h3, null, null, eta)), $$sc.h3.h3.h2), tm))))))))))))))))))))))))))))))))))); break; } } break; } case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _3 ) => ((((("SKIP ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" because unify error ")) + (Lib_Types_errorMsg($$sc2.h2))) + (""))), ( _3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_HasIO$20Lib_Types_M$2CliftIO(null, Prelude_primPutStrLn((((("SKIP ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" because unify error ")) + (Lib_Types_errorMsg($$sc2.h2))) + (""))), ( _4 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Prelude_Nothing(null)))))); } }); } break; default: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_tryError(null, Lib_Elab_unify($$sc.h2.h1, 1, $$sc.h3.h2, _$$3)), ( $$sc2 ) => { switch ($$sc2.tag) { case 1: { const sc$$50 = Prelude_findIndex$27(null, ( _$$5 ) => (Prelude_jsEq(null, _$$2, _$$5.h2)), $$sc.h2.h2); switch (sc$$50.tag) { case 1: return Lib_Types_MkM(null, ( _3 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$0.h4, (("") + (_$$2)) + (" not is scope?"))), eta)))); case 0: { const lvl = ((Prelude_length$27(null, $$sc.h2.h1)) - (sc$$50.h1)) - (1); const scon = Prelude__$2C_(null, null, lvl, Lib_Types_VRef(_$$0.h4, _$$4.h2, $$sc.h3.h3.h3)); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _3 ) => ((("scty ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$3))) + (""))), ( _3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _4 ) => ((("UNIFY results ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( eta ) => (Prelude_Prelude_Show$20$28Prelude__$D7_$20BND$3A3$20BND$3A2$29$2Cshow(null, null, Prelude_Prelude_Show$20Prim_Int, Lib_Types_Prelude_Show$20Lib_Types_Val, eta)), $$sc2.h2.h0)))) + (""))), ( _4 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _5 ) => ((("before types: ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( eta ) => (Prelude_Prelude_Show$20$28Prelude__$D7_$20BND$3A3$20BND$3A2$29$2Cshow(null, null, Prelude_Prelude_Show$20Prim_String, Lib_Types_Prelude_Show$20Lib_Types_Val, eta)), $$sc.h2.h2)))) + (""))), ( _5 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _6 ) => ((("before env: ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, $$sc.h2.h1)))) + (""))), ( _6 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _7 ) => ((("SC CONSTRAINT: ") + (Prelude_Prelude_Show$20$28Prelude__$D7_$20BND$3A3$20BND$3A2$29$2Cshow(null, null, Prelude_Prelude_Show$20Prim_Int, Lib_Types_Prelude_Show$20Lib_Types_Val, scon))) + (""))), ( _7 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_updateContext($$sc.h2, Prelude__$3A$3A_(null, scon, $$sc2.h2.h0)), ( ctx$27 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _8 ) => ((("context types: ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( eta ) => (Prelude_Prelude_Show$20$28Prelude__$D7_$20BND$3A3$20BND$3A2$29$2Cshow(null, null, Prelude_Prelude_Show$20Prim_String, Lib_Types_Prelude_Show$20Lib_Types_Val, eta)), ctx$27.h2)))) + (""))), ( _8 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _9 ) => ((("context env: ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, ctx$27.h1)))) + (""))), ( _9 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _10 ) => ((((((("(dcon ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" ty ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow($$sc.h3.h2))) + (" scty ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$3))) + (""))), ( _10 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _11 ) => ((((("(dcon ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (") (vars ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Elab_Prelude_Show$20Lib_Elab_Bind$2Cshow, $$sc.h3.h3.h2)))) + (") clauses were"))), ( _11 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, _$$1.h0, ( x ) => (Lib_Types_log(2, ( _12 ) => (((" ") + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Clause$2Cshow(x))) + (""))))), ( _12 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Functor$20Lib_Types_M$2Cmap(null, null, ( eta ) => (Prelude_mapMaybe(null, null, ( _$$11 ) => (_$$11), eta)), Prelude_Prelude_Traversable$20Prelude_List$2Ctraverse(null, null, null, Lib_Types_Prelude_Applicative$20Lib_Types_M, ( eta ) => (Lib_Elab_buildCase_constrainSpine_getName_makeConstr_rewriteConstraint_rewriteClause(_$$0, _$$1, _$$2, _$$3, _$$4, _$$4.h0, _$$4.h1, _$$4.h2, _$$4.h3, _$$4.h3.h0, _$$4.h3.h1, _$$4.h3.h2, _$$4.h3.h3, null, null, null, null, null, _$$3.h1, $$sc.h3.h3.h2, eta)), _$$1.h0)), ( clauses ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _13 ) => ("and now:")), ( _13 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, clauses, ( x ) => (Lib_Types_log(2, ( _14 ) => (((" ") + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Clause$2Cshow(x))) + (""))))), ( _14 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_when(null, Lib_Types_Prelude_Applicative$20Lib_Types_M, Prelude_jsEq(null, Prelude_length$27(null, clauses), 0), ( _15 ) => (Lib_Types_MkM(null, ( _16 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$0.h4, (((("Missing case for ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" splitting ")) + (_$$2)) + (""))), eta)))))), ( _15 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_buildTree(ctx$27, Lib_Elab_MkProb(clauses, _$$1.h1)), ( tm ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Prelude_Just(null, Lib_Types_CaseCons(_$$4.h2, Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( eta ) => (Lib_Elab_buildCase_constrainSpine_getName(_$$0, _$$1, _$$2, _$$3, _$$4, _$$4.h0, _$$4.h1, _$$4.h2, _$$4.h3, _$$4.h3.h0, _$$4.h3.h1, _$$4.h3.h2, _$$4.h3.h3, null, null, eta)), $$sc.h3.h3.h2), tm))))))))))))))))))))))))))))))))))); break; } } break; } case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _3 ) => ((((("SKIP ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" because unify error ")) + (Lib_Types_errorMsg($$sc2.h2))) + (""))), ( _3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_HasIO$20Lib_Types_M$2CliftIO(null, Prelude_primPutStrLn((((("SKIP ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$4.h2))) + (" because unify error ")) + (Lib_Types_errorMsg($$sc2.h2))) + (""))), ( _4 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Prelude_Nothing(null)))))); } }); } break; } default: return Lib_Types_MkM(null, ( _3 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Types_getValFC(_$$3), (("case split on non-inductive ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$3))) + (""))), eta)))); } }); default: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Prelude_Nothing(null)); } })))))))))); @@ -707,7 +710,7 @@ const Lib_Elab_REC_lookupName_go = ( arg ) => { switch (arg.h4.tag) { case 1: { const Lib_Elab_findSplit = ( _$$0 ) => (bouncer(Lib_Elab_REC_findSplit, { tag: 1, h0: _$$0 })); const Lib_Elab_REC_findSplit = ( arg ) => { switch (arg.h0.tag) { case 1: switch (arg.h0.h1.h3.tag) { case 3: return { tag: 0, h0: Prelude_Just(null, arg.h0.h1) }; case 1: return { tag: 0, h0: Prelude_Just(null, arg.h0.h1) }; default: return { tag: 1, h0: arg.h0.h2 }; } break; case 0: return { tag: 0, h0: Prelude_Nothing(null) }; } }; const Lib_Elab_introClause = ( _$$0, _$$1, _$$2 ) => { switch (_$$2.h2.tag) { case 1: { const sc$$10 = Lib_Types_Prelude_Eq$20Lib_Types_Icit$2C_$3D$3D_(_$$1, Lib_Syntax_getIcit(_$$2.h2.h1)); switch (sc$$10) { case 1: { const sc$$11 = Lib_Types_Prelude_Eq$20Lib_Types_Icit$2C_$3D$3D_(_$$1, 0); switch (sc$$11) { case 1: { const sc$$12 = Lib_Types_Prelude_Eq$20Lib_Types_Icit$2C_$3D$3D_(_$$1, 2); switch (sc$$12) { case 1: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$2.h0, (((((("Explicit arg and ") + (Lib_Types_Prelude_Show$20Lib_Types_Icit$2Cshow(Lib_Syntax_getIcit(_$$2.h2.h1)))) + (" pattern ")) + (_$$0)) + (" ")) + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Pattern$2Cshow(_$$2.h2.h1))) + (""))), eta)))); case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_MkClause(_$$2.h0, Prelude__$3A$3A_(null, Prelude__$2C_(null, null, _$$0, Lib_Syntax_PatWild(_$$2.h0, 2)), _$$2.h1), Prelude__$3A$3A_(null, _$$2.h2.h1, _$$2.h2.h2), _$$2.h3)); } break; } case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_MkClause(_$$2.h0, Prelude__$3A$3A_(null, Prelude__$2C_(null, null, _$$0, Lib_Syntax_PatWild(_$$2.h0, 0)), _$$2.h1), Prelude__$3A$3A_(null, _$$2.h2.h1, _$$2.h2.h2), _$$2.h3)); } break; } case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_MkClause(_$$2.h0, Prelude__$3A$3A_(null, Prelude__$2C_(null, null, _$$0, _$$2.h2.h1), _$$2.h1), _$$2.h2.h2, _$$2.h3)); } break; } case 0: switch (_$$1) { case 2: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_MkClause(_$$2.h0, Prelude__$3A$3A_(null, Prelude__$2C_(null, null, _$$0, Lib_Syntax_PatWild(_$$2.h0, 2)), _$$2.h1), Prelude_Nil(null), _$$2.h3)); case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_MkClause(_$$2.h0, Prelude__$3A$3A_(null, Prelude__$2C_(null, null, _$$0, Lib_Syntax_PatWild(_$$2.h0, 0)), _$$2.h1), Prelude_Nil(null), _$$2.h3)); default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$2.h0, "Clause size doesn't match")), eta)))); } break; } }; -const Lib_Elab_mkPat = ( _$$0 ) => { switch (_$$0.h2.tag) { case 14: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_mkPat(Prelude__$2C_(null, null, _$$0.h2.h2, _$$0.h3)), ( pat ) => { switch (pat.tag) { case 1: switch (pat.h4.tag) { case 1: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_PatCon(pat.h0, pat.h1, pat.h2, pat.h3, Prelude_Just(null, _$$0.h2.h1))); default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(pat.h0, (("Double as pattern ") + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Raw$2Cshow(_$$0.h2.h2))) + (""))), eta)))); } break; default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$0.h2.h0, (("Can't put as on non-constructor ") + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Raw$2Cshow(_$$0.h2.h2))) + (""))), eta)))); } }); default: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$6 = Lib_Elab_splitArgs(_$$0.h2, Prelude_Nil(null)); switch (sc$$6.h2.tag) { case 9: switch (sc$$6.h3.tag) { case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_PatWild(sc$$6.h2.h0, _$$0.h3)); default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(sc$$6.h2.h0, "implicit pat can't be applied to arguments")), eta)))); } break; case 7: switch (sc$$6.h3.tag) { case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_PatLit(sc$$6.h2.h0, sc$$6.h2.h1)); default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(sc$$6.h2.h0, "lit cannot be applied to arguments")), eta)))); } break; case 0: { const sc$$13 = Lib_TopContext_lookupRaw(sc$$6.h2.h1, top); switch (sc$$13.tag) { case 0: switch (sc$$13.h1.h3.tag) { case 2: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_Prelude_Traversable$20Prelude_List$2Ctraverse(null, null, null, Lib_Types_Prelude_Applicative$20Lib_Types_M, Lib_Elab_mkPat, sc$$6.h3), ( bpat ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_PatCon(sc$$6.h2.h0, _$$0.h3, sc$$13.h1.h1, bpat, Prelude_Nothing(null))))); default: switch (sc$$6.h3.tag) { case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_PatVar(sc$$6.h2.h0, _$$0.h3, sc$$6.h2.h1)); default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$0.h2), "patvar applied to args")), eta)))); } break; } break; default: switch (sc$$6.h3.tag) { case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_PatVar(sc$$6.h2.h0, _$$0.h3, sc$$6.h2.h1)); default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$0.h2), "patvar applied to args")), eta)))); } break; } break; } default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(sc$$6.h2), (("expected pat var or constructor, got ") + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Raw$2Cshow(sc$$6.h2))) + (""))), eta)))); } }); } }; +const Lib_Elab_mkPat = ( _$$0 ) => { switch (_$$0.h2.tag) { case 14: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_mkPat(Prelude__$2C_(null, null, _$$0.h2.h2, _$$0.h3)), ( pat ) => { switch (pat.tag) { case 1: switch (pat.h4.tag) { case 1: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_PatCon(pat.h0, pat.h1, pat.h2, pat.h3, Prelude_Just(null, _$$0.h2.h1))); default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(pat.h0, (("Double as pattern ") + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Raw$2Cshow(_$$0.h2.h2))) + (""))), eta)))); } break; default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$0.h2.h0, (("Can't put as on non-constructor ") + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Raw$2Cshow(_$$0.h2.h2))) + (""))), eta)))); } }); default: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$6 = Lib_Elab_splitArgs(_$$0.h2, Prelude_Nil(null)); switch (sc$$6.h2.tag) { case 9: switch (sc$$6.h3.tag) { case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_PatWild(sc$$6.h2.h0, _$$0.h3)); default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(sc$$6.h2.h0, "implicit pat can't be applied to arguments")), eta)))); } break; case 7: switch (sc$$6.h3.tag) { case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_PatLit(sc$$6.h2.h0, sc$$6.h2.h1)); default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(sc$$6.h2.h0, "lit cannot be applied to arguments")), eta)))); } break; case 0: { const sc$$13 = Lib_TopContext_lookupRaw(sc$$6.h2.h1, top); switch (sc$$13.tag) { case 0: switch (sc$$13.h1.h3.tag) { case 2: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_Prelude_Traversable$20Prelude_List$2Ctraverse(null, null, null, Lib_Types_Prelude_Applicative$20Lib_Types_M, Lib_Elab_mkPat, sc$$6.h3), ( bpat ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_PatCon(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$0.h2), _$$0.h3, sc$$13.h1.h1, bpat, Prelude_Nothing(null))))); default: switch (sc$$6.h3.tag) { case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_PatVar(sc$$6.h2.h0, _$$0.h3, sc$$6.h2.h1)); default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$0.h2), "patvar applied to args")), eta)))); } break; } break; default: switch (sc$$6.h3.tag) { case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Syntax_PatVar(sc$$6.h2.h0, _$$0.h3, sc$$6.h2.h1)); default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$0.h2), "patvar applied to args")), eta)))); } break; } break; } default: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(sc$$6.h2), (("expected pat var or constructor, got ") + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Raw$2Cshow(sc$$6.h2))) + (""))), eta)))); } }); } }; const Lib_Syntax_PatCon = ( h0, h1, h2, h3, h4 ) => ({ tag: 1, h0: h0, h1: h1, h2: h2, h3: h3, h4: h4 }); const Lib_Syntax_PatLit = ( h0, h1 ) => ({ tag: 3, h0: h0, h1: h1 }); const Lib_Elab_splitArgs = ( _$$0, _$$1 ) => (bouncer(Lib_Elab_REC_splitArgs, { tag: 1, h0: _$$0, h1: _$$1 })); @@ -859,15 +862,16 @@ const Prelude_map = ( m$$0, _$$1 ) => (( a ) => (( b ) => (_$$1.h1(null)(null))) const Lib_Parser_optional = ( a$$0, _$$1 ) => (Lib_Parser_Impl_Prelude_Alternative$20Lib_Parser_Impl_Parser$2C_$3C$7C$3E_(null, Lib_Parser_Impl_Prelude_Functor$20Lib_Parser_Impl_Parser$2Cmap(null, null, ( eta ) => (Prelude_Just(null, eta)), _$$1), Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Prelude_Nothing(null)))); const Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind = ( a$$0, b$$1, _$$2, _$$3 ) => (Lib_Parser_Impl_P(null, ( last ) => (( toks ) => (( com ) => (( ops ) => (( col ) => { const sc$$11 = _$$2.h1(last)(toks)(com)(ops)(col); switch (sc$$11.tag) { case 1: return Lib_Parser_Impl_Fail(null, sc$$11.h1, sc$$11.h2, sc$$11.h3, sc$$11.h4, sc$$11.h5, sc$$11.h6); case 0: return Lib_Parser_Impl_runP(null, _$$3(sc$$11.h1))(sc$$11.h2)(sc$$11.h3)(sc$$11.h4)(sc$$11.h5)(col); } })))))); const Lib_Parser_Impl_runP = ( a$$0, _$$1 ) => (_$$1.h1); -const Lib_Parser_term_apply = ( _, _$$1, _$$2 ) => { switch (_$$2.tag) { case 1: return Lib_Syntax_RApp(_$$2.h1.h2, _$$1, Lib_Parser_term_apply(_, _$$2.h1.h3, _$$2.h2), 1); case 0: return _$$1; } }; +const Lib_Parser_term_apply = ( _, _$$1, _$$2 ) => { switch (_$$2.tag) { case 1: { const u = Lib_Parser_term_apply(_, _$$2.h1.h3, _$$2.h2); const _sc$$1 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(u); const _sc$$2 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$1); return Lib_Syntax_RApp(Lib_Common_MkFC(_sc$$2.h0, Lib_Common_Prelude_Add$20Lib_Common_Bounds$2C_$2B_(_sc$$2.h1, _sc$$1.h1)), _$$1, u, 1); break; } case 0: return _$$1; } }; +const Lib_Common_Prelude_Add$20Lib_Common_Bounds$2C_$2B_ = ( _$$0, _$$1 ) => { let a$27; const sc$$2 = Prelude__$7C$7C_(Prelude_Prelude_Eq$20Prelude_Ordering$2C_$3D$3D_(Prelude_jsCompare(null, _$$0.h0, _$$1.h0), 0), Prelude__$26$26_(Prelude_jsEq(null, _$$0.h0, _$$1.h0), Prelude_Prelude_Eq$20Prelude_Ordering$2C_$3D$3D_(Prelude_jsCompare(null, _$$0.h1, _$$1.h1), 0))); switch (sc$$2) { case 1: { a$27 = _$$1; break; } case 0: { a$27 = _$$0; break; } } let b$27; const sc$$3 = Prelude__$7C$7C_(Prelude_Prelude_Eq$20Prelude_Ordering$2C_$3D$3D_(Prelude_jsCompare(null, _$$0.h2, _$$1.h2), 0), Prelude__$26$26_(Prelude_jsEq(null, _$$0.h2, _$$1.h2), Prelude_Prelude_Eq$20Prelude_Ordering$2C_$3D$3D_(Prelude_jsCompare(null, _$$0.h3, _$$1.h3), 0))); switch (sc$$3) { case 1: { b$27 = _$$0; break; } case 0: { b$27 = _$$1; break; } } return Lib_Common_MkBounds(a$27.h0, a$27.h1, b$27.h2, b$27.h3); }; const Lib_Parser_Impl_fail = ( a$$0, _$$1 ) => (Lib_Parser_Impl_P(null, ( last ) => (( toks ) => (( com ) => (( ops ) => (( col ) => (Lib_Parser_Impl_Fail(null, 1, Lib_Parser_Impl_perror(col.h0, toks, _$$1), last, toks, com, ops)))))))); -const Lib_Parser_pratt = ( _$$0, _$$1, _$$2, _$$3, _$$4 ) => (Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_pratt_projectHead_runProject_runRule_runPrefix(_$$0, _$$1, _$$2, _$$3, _$$4, null, null, null, null, _$$2, _$$3, _$$4), ( $$sc ) => { const sc$$15 = Lib_Parser_pratt_projectHead(_$$0, _$$1, _$$2, _$$3, _$$4, null, $$sc.h2, $$sc.h3); const spine = Lib_Parser_pratt_projectHead_runProject(_$$0, _$$1, _$$2, _$$3, _$$4, null, null, sc$$15.h3); switch (spine.tag) { case 1: switch (spine.h1.h2) { case 1: switch (spine.h1.h3.h3.tag) { case 0: { const sc$$35 = Prelude_jsEq(null, spine.h1.h3.h3.h1, _$$2); switch (sc$$35) { case 1: { const sc$$36 = Data_SortedMap_lookupMap$27(null, null, spine.h1.h3.h3.h1, _$$0); switch (sc$$36.tag) { case 1: { const sc$$38 = Prelude_isPrefixOf(".", spine.h1.h3.h3.h1); switch (sc$$38) { case 1: return Lib_Parser_pratt(_$$0, _$$1, _$$2, Lib_Syntax_RApp(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(sc$$15.h2), sc$$15.h2, spine.h1.h3.h3, 1), spine.h2); case 0: return Lib_Parser_pratt(_$$0, _$$1, _$$2, Lib_Syntax_RApp(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(spine.h1.h3.h3), spine.h1.h3.h3, sc$$15.h2, 1), spine.h2); } break; } case 0: switch (sc$$36.h1.h3) { case 1: { const sc$$44 = Prelude_Prelude_Eq$20Prelude_Ordering$2C_$3D$3D_(Prelude_jsCompare(null, sc$$36.h1.h1, _$$1), 0); switch (sc$$44) { case 1: return Lib_Parser_pratt_projectHead_runProject_runRule(_$$0, _$$1, _$$2, _$$3, _$$4, null, null, null, sc$$36.h1.h1, sc$$36.h1.h2, _$$2, sc$$36.h1.h4, Lib_Syntax_RApp(spine.h1.h3.h2, Lib_Syntax_RVar(spine.h1.h3.h2, sc$$36.h1.h0), sc$$15.h2, 1), spine.h2); case 0: return Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Prelude__$2C_(null, null, sc$$15.h2, spine)); } break; } default: return Lib_Parser_Impl_fail(null, "expected operator"); } break; } break; } case 0: return Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Prelude__$2C_(null, null, sc$$15.h2, spine)); } break; } default: return Lib_Parser_pratt(_$$0, _$$1, _$$2, Lib_Syntax_RApp(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(sc$$15.h2), sc$$15.h2, spine.h1.h3.h3, spine.h1.h2), spine.h2); } break; default: return Lib_Parser_pratt(_$$0, _$$1, _$$2, Lib_Syntax_RApp(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(sc$$15.h2), sc$$15.h2, spine.h1.h3.h3, spine.h1.h2), spine.h2); } break; case 0: return Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Prelude__$2C_(null, null, sc$$15.h2, Prelude_Nil(null))); } })); -const Lib_Parser_pratt_projectHead_runProject_runRule = ( _, _1, _2, _3, _4, _5, _6, _7, _$$8, _$$9, _$$10, _$$11, _$$12, _$$13 ) => { switch (_$$11.tag) { case 1: switch (_$$11.h1) { case "": switch (_$$11.h2.tag) { case 0: { let pr; switch (_$$9) { case 1: { pr = _$$8; break; } default: { pr = (_$$8) + (1); break; } } switch (_$$13.tag) { case 1: return Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_pratt(_, pr, _$$10, _$$13.h1.h3.h3, _$$13.h2), ( $$sc ) => (Lib_Parser_pratt(_, _1, _$$10, Lib_Syntax_RApp(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$12), _$$12, $$sc.h2, 1), $$sc.h3))); default: return Lib_Parser_Impl_fail(null, "trailing operator"); } break; } default: switch (_$$13.tag) { case 1: return Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_pratt(_, 0, _$$11.h1, _$$13.h1.h3.h3, _$$13.h2), ( $$sc ) => { switch ($$sc.h3.tag) { case 1: switch ($$sc.h3.h1.h3.h3.tag) { case 0: { const sc$$49 = Prelude_jsEq(null, $$sc.h3.h1.h3.h3.h1, _$$11.h1); switch (sc$$49) { case 1: return Lib_Parser_Impl_fail(null, (("expected ") + (_$$11.h1)) + ("")); case 0: return Lib_Parser_pratt_projectHead_runProject_runRule(_, _1, _2, _3, _4, _5, _6, _7, _$$8, _$$9, _$$10, _$$11.h2, Lib_Syntax_RApp(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$12), _$$12, $$sc.h2, 1), $$sc.h3.h2); } break; } default: return Lib_Parser_Impl_fail(null, (("expected ") + (_$$11.h1)) + ("")); } break; default: return Lib_Parser_Impl_fail(null, (("expected ") + (_$$11.h1)) + ("")); } }); case 0: return Lib_Parser_Impl_fail(null, "short"); } break; } break; default: switch (_$$13.tag) { case 1: return Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_pratt(_, 0, _$$11.h1, _$$13.h1.h3.h3, _$$13.h2), ( $$sc ) => { switch ($$sc.h3.tag) { case 1: switch ($$sc.h3.h1.h3.h3.tag) { case 0: { const sc$$49 = Prelude_jsEq(null, $$sc.h3.h1.h3.h3.h1, _$$11.h1); switch (sc$$49) { case 1: return Lib_Parser_Impl_fail(null, (("expected ") + (_$$11.h1)) + ("")); case 0: return Lib_Parser_pratt_projectHead_runProject_runRule(_, _1, _2, _3, _4, _5, _6, _7, _$$8, _$$9, _$$10, _$$11.h2, Lib_Syntax_RApp(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$12), _$$12, $$sc.h2, 1), $$sc.h3.h2); } break; } default: return Lib_Parser_Impl_fail(null, (("expected ") + (_$$11.h1)) + ("")); } break; default: return Lib_Parser_Impl_fail(null, (("expected ") + (_$$11.h1)) + ("")); } }); case 0: return Lib_Parser_Impl_fail(null, "short"); } break; } break; case 0: return Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Prelude__$2C_(null, null, _$$12, _$$13)); } }; +const Lib_Parser_pratt = ( _$$0, _$$1, _$$2, _$$3, _$$4 ) => (Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_pratt_projectHead_runProject_runRule_runPrefix(_$$0, _$$1, _$$2, _$$3, _$$4, null, null, null, null, _$$2, _$$3, _$$4), ( $$sc ) => { const sc$$15 = Lib_Parser_pratt_projectHead(_$$0, _$$1, _$$2, _$$3, _$$4, null, $$sc.h2, $$sc.h3); const spine = Lib_Parser_pratt_projectHead_runProject(_$$0, _$$1, _$$2, _$$3, _$$4, null, null, sc$$15.h3); switch (spine.tag) { case 1: switch (spine.h1.h2) { case 1: switch (spine.h1.h3.h3.tag) { case 0: { const sc$$35 = Prelude_jsEq(null, spine.h1.h3.h3.h1, _$$2); switch (sc$$35) { case 1: { const sc$$36 = Data_SortedMap_lookupMap$27(null, null, spine.h1.h3.h3.h1, _$$0); switch (sc$$36.tag) { case 1: { const sc$$38 = Prelude_isPrefixOf(".", spine.h1.h3.h3.h1); switch (sc$$38) { case 1: { const _sc$$10 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(spine.h1.h3.h3); const _sc$$11 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(sc$$15.h2); return Lib_Parser_pratt(_$$0, _$$1, _$$2, Lib_Syntax_RApp(Lib_Common_MkFC(_sc$$11.h0, Lib_Common_Prelude_Add$20Lib_Common_Bounds$2C_$2B_(_sc$$11.h1, _sc$$10.h1)), sc$$15.h2, spine.h1.h3.h3, 1), spine.h2); break; } case 0: { const _sc$$10 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(spine.h1.h3.h3); const _sc$$11 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(sc$$15.h2); return Lib_Parser_pratt(_$$0, _$$1, _$$2, Lib_Syntax_RApp(Lib_Common_MkFC(_sc$$11.h0, Lib_Common_Prelude_Add$20Lib_Common_Bounds$2C_$2B_(_sc$$11.h1, _sc$$10.h1)), spine.h1.h3.h3, sc$$15.h2, 1), spine.h2); break; } } break; } case 0: switch (sc$$36.h1.h3) { case 1: { const sc$$44 = Prelude_Prelude_Eq$20Prelude_Ordering$2C_$3D$3D_(Prelude_jsCompare(null, sc$$36.h1.h1, _$$1), 0); switch (sc$$44) { case 1: { const _sc$$22 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(sc$$15.h2); return Lib_Parser_pratt_projectHead_runProject_runRule(_$$0, _$$1, _$$2, _$$3, _$$4, null, null, null, sc$$36.h1.h1, sc$$36.h1.h2, _$$2, sc$$36.h1.h4, Lib_Syntax_RApp(Lib_Common_MkFC(_sc$$22.h0, Lib_Common_Prelude_Add$20Lib_Common_Bounds$2C_$2B_(_sc$$22.h1, spine.h1.h3.h2.h1)), Lib_Syntax_RVar(spine.h1.h3.h2, sc$$36.h1.h0), sc$$15.h2, 1), spine.h2); break; } case 0: return Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Prelude__$2C_(null, null, sc$$15.h2, spine)); } break; } default: return Lib_Parser_Impl_fail(null, "expected operator"); } break; } break; } case 0: return Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Prelude__$2C_(null, null, sc$$15.h2, spine)); } break; } default: { const _sc$$10 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(spine.h1.h3.h3); const _sc$$11 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(sc$$15.h2); return Lib_Parser_pratt(_$$0, _$$1, _$$2, Lib_Syntax_RApp(Lib_Common_MkFC(_sc$$11.h0, Lib_Common_Prelude_Add$20Lib_Common_Bounds$2C_$2B_(_sc$$11.h1, _sc$$10.h1)), sc$$15.h2, spine.h1.h3.h3, spine.h1.h2), spine.h2); break; } } break; default: { const _sc$$9 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(spine.h1.h3.h3); const _sc$$10 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(sc$$15.h2); return Lib_Parser_pratt(_$$0, _$$1, _$$2, Lib_Syntax_RApp(Lib_Common_MkFC(_sc$$10.h0, Lib_Common_Prelude_Add$20Lib_Common_Bounds$2C_$2B_(_sc$$10.h1, _sc$$9.h1)), sc$$15.h2, spine.h1.h3.h3, spine.h1.h2), spine.h2); break; } } break; case 0: return Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Prelude__$2C_(null, null, sc$$15.h2, Prelude_Nil(null))); } })); +const Lib_Parser_pratt_projectHead_runProject_runRule = ( _, _1, _2, _3, _4, _5, _6, _7, _$$8, _$$9, _$$10, _$$11, _$$12, _$$13 ) => { switch (_$$11.tag) { case 1: switch (_$$11.h1) { case "": switch (_$$11.h2.tag) { case 0: { let pr; switch (_$$9) { case 1: { pr = _$$8; break; } default: { pr = (_$$8) + (1); break; } } switch (_$$13.tag) { case 1: return Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_pratt(_, pr, _$$10, _$$13.h1.h3.h3, _$$13.h2), ( $$sc ) => { const _sc$$10 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC($$sc.h2); const _sc$$11 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$12); return Lib_Parser_pratt(_, _1, _$$10, Lib_Syntax_RApp(Lib_Common_MkFC(_sc$$11.h0, Lib_Common_Prelude_Add$20Lib_Common_Bounds$2C_$2B_(_sc$$11.h1, _sc$$10.h1)), _$$12, $$sc.h2, 1), $$sc.h3); }); default: return Lib_Parser_Impl_fail(null, "trailing operator"); } break; } default: switch (_$$13.tag) { case 1: return Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_pratt(_, 0, _$$11.h1, _$$13.h1.h3.h3, _$$13.h2), ( $$sc ) => { switch ($$sc.h3.tag) { case 1: switch ($$sc.h3.h1.h3.h3.tag) { case 0: { const sc$$49 = Prelude_jsEq(null, $$sc.h3.h1.h3.h3.h1, _$$11.h1); switch (sc$$49) { case 1: return Lib_Parser_Impl_fail(null, (("expected ") + (_$$11.h1)) + ("")); case 0: { const _sc$$23 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC($$sc.h2); const _sc$$24 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$12); return Lib_Parser_pratt_projectHead_runProject_runRule(_, _1, _2, _3, _4, _5, _6, _7, _$$8, _$$9, _$$10, _$$11.h2, Lib_Syntax_RApp(Lib_Common_MkFC(_sc$$24.h0, Lib_Common_Prelude_Add$20Lib_Common_Bounds$2C_$2B_(_sc$$24.h1, _sc$$23.h1)), _$$12, $$sc.h2, 1), $$sc.h3.h2); break; } } break; } default: return Lib_Parser_Impl_fail(null, (("expected ") + (_$$11.h1)) + ("")); } break; default: return Lib_Parser_Impl_fail(null, (("expected ") + (_$$11.h1)) + ("")); } }); case 0: return Lib_Parser_Impl_fail(null, "short"); } break; } break; default: switch (_$$13.tag) { case 1: return Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_pratt(_, 0, _$$11.h1, _$$13.h1.h3.h3, _$$13.h2), ( $$sc ) => { switch ($$sc.h3.tag) { case 1: switch ($$sc.h3.h1.h3.h3.tag) { case 0: { const sc$$49 = Prelude_jsEq(null, $$sc.h3.h1.h3.h3.h1, _$$11.h1); switch (sc$$49) { case 1: return Lib_Parser_Impl_fail(null, (("expected ") + (_$$11.h1)) + ("")); case 0: { const _sc$$22 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC($$sc.h2); const _sc$$23 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$12); return Lib_Parser_pratt_projectHead_runProject_runRule(_, _1, _2, _3, _4, _5, _6, _7, _$$8, _$$9, _$$10, _$$11.h2, Lib_Syntax_RApp(Lib_Common_MkFC(_sc$$23.h0, Lib_Common_Prelude_Add$20Lib_Common_Bounds$2C_$2B_(_sc$$23.h1, _sc$$22.h1)), _$$12, $$sc.h2, 1), $$sc.h3.h2); break; } } break; } default: return Lib_Parser_Impl_fail(null, (("expected ") + (_$$11.h1)) + ("")); } break; default: return Lib_Parser_Impl_fail(null, (("expected ") + (_$$11.h1)) + ("")); } }); case 0: return Lib_Parser_Impl_fail(null, "short"); } break; } break; case 0: return Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Prelude__$2C_(null, null, _$$12, _$$13)); } }; const Prelude_isPrefixOf = (pfx, s) => s.startsWith(pfx) ? Prelude_True : Prelude_False; const Lib_Parser_pratt_projectHead_runProject = ( _, _1, _2, _3, _4, _5, _6, _$$7 ) => (bouncer(Lib_Parser_REC_pratt_projectHead_runProject, { tag: 1, h0: _, h1: _1, h2: _2, h3: _3, h4: _4, h5: _5, h6: _6, h7: _$$7 })); -const Lib_Parser_REC_pratt_projectHead_runProject = ( arg ) => { switch (arg.h7.tag) { case 1: switch (arg.h7.h1.h2) { case 1: switch (arg.h7.h2.tag) { case 1: switch (arg.h7.h2.h1.h2) { case 1: switch (arg.h7.h2.h1.h3.h3.tag) { case 0: { const sc$$32 = Prelude_isPrefixOf(".", arg.h7.h2.h1.h3.h3.h1); switch (sc$$32) { case 1: return { tag: 0, h0: Prelude__$3A$3A_(null, arg.h7.h1, Prelude__$3A$3A_(null, arg.h7.h2.h1, arg.h7.h2.h2)) }; case 0: return { tag: 1, h0: arg.h0, h1: arg.h1, h2: arg.h2, h3: arg.h3, h4: arg.h4, h5: arg.h5, h6: arg.h6, h7: Prelude__$3A$3A_(null, Prelude__$2C_(null, null, 1, Prelude__$2C_(null, null, arg.h7.h1.h3.h2, Lib_Syntax_RApp(arg.h7.h2.h1.h3.h3.h0, Lib_Syntax_RVar(arg.h7.h2.h1.h3.h3.h0, arg.h7.h2.h1.h3.h3.h1), arg.h7.h1.h3.h3, 1))), arg.h7.h2.h2) }; } break; } default: return { tag: 0, h0: arg.h7 }; } break; default: return { tag: 0, h0: arg.h7 }; } break; default: return { tag: 0, h0: arg.h7 }; } break; default: return { tag: 0, h0: arg.h7 }; } break; default: return { tag: 0, h0: arg.h7 }; } }; +const Lib_Parser_REC_pratt_projectHead_runProject = ( arg ) => { switch (arg.h7.tag) { case 1: switch (arg.h7.h1.h2) { case 1: switch (arg.h7.h2.tag) { case 1: switch (arg.h7.h2.h1.h2) { case 1: switch (arg.h7.h2.h1.h3.h3.tag) { case 0: { const sc$$32 = Prelude_isPrefixOf(".", arg.h7.h2.h1.h3.h3.h1); switch (sc$$32) { case 1: return { tag: 0, h0: Prelude__$3A$3A_(null, arg.h7.h1, Prelude__$3A$3A_(null, arg.h7.h2.h1, arg.h7.h2.h2)) }; case 0: { const _sc$$16 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(arg.h7.h1.h3.h3); return { tag: 1, h0: arg.h0, h1: arg.h1, h2: arg.h2, h3: arg.h3, h4: arg.h4, h5: arg.h5, h6: arg.h6, h7: Prelude__$3A$3A_(null, Prelude__$2C_(null, null, 1, Prelude__$2C_(null, null, arg.h7.h1.h3.h2, Lib_Syntax_RApp(Lib_Common_MkFC(arg.h7.h2.h1.h3.h3.h0.h0, Lib_Common_Prelude_Add$20Lib_Common_Bounds$2C_$2B_(arg.h7.h2.h1.h3.h3.h0.h1, _sc$$16.h1)), Lib_Syntax_RVar(arg.h7.h2.h1.h3.h3.h0, arg.h7.h2.h1.h3.h3.h1), arg.h7.h1.h3.h3, 1))), arg.h7.h2.h2) }; break; } } break; } default: return { tag: 0, h0: arg.h7 }; } break; default: return { tag: 0, h0: arg.h7 }; } break; default: return { tag: 0, h0: arg.h7 }; } break; default: return { tag: 0, h0: arg.h7 }; } break; default: return { tag: 0, h0: arg.h7 }; } }; const Lib_Parser_pratt_projectHead = ( _, _1, _2, _3, _4, _5, _$$6, _$$7 ) => (bouncer(Lib_Parser_REC_pratt_projectHead, { tag: 1, h0: _, h1: _1, h2: _2, h3: _3, h4: _4, h5: _5, h6: _$$6, h7: _$$7 })); -const Lib_Parser_REC_pratt_projectHead = ( arg ) => { switch (arg.h7.tag) { case 1: switch (arg.h7.h1.h2) { case 1: switch (arg.h7.h1.h3.h3.tag) { case 0: { const sc$$21 = Prelude_isPrefixOf(".", arg.h7.h1.h3.h3.h1); switch (sc$$21) { case 1: return { tag: 0, h0: Prelude__$2C_(null, null, arg.h6, arg.h7) }; case 0: return { tag: 1, h0: arg.h0, h1: arg.h1, h2: arg.h2, h3: arg.h3, h4: arg.h4, h5: arg.h5, h6: Lib_Syntax_RApp(arg.h7.h1.h3.h3.h0, Lib_Syntax_RVar(arg.h7.h1.h3.h3.h0, arg.h7.h1.h3.h3.h1), arg.h6, 1), h7: arg.h7.h2 }; } break; } default: return { tag: 0, h0: Prelude__$2C_(null, null, arg.h6, arg.h7) }; } break; default: return { tag: 0, h0: Prelude__$2C_(null, null, arg.h6, arg.h7) }; } break; default: return { tag: 0, h0: Prelude__$2C_(null, null, arg.h6, arg.h7) }; } }; +const Lib_Parser_REC_pratt_projectHead = ( arg ) => { switch (arg.h7.tag) { case 1: switch (arg.h7.h1.h2) { case 1: switch (arg.h7.h1.h3.h3.tag) { case 0: { const sc$$21 = Prelude_isPrefixOf(".", arg.h7.h1.h3.h3.h1); switch (sc$$21) { case 1: return { tag: 0, h0: Prelude__$2C_(null, null, arg.h6, arg.h7) }; case 0: { const _sc$$5 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(arg.h6); return { tag: 1, h0: arg.h0, h1: arg.h1, h2: arg.h2, h3: arg.h3, h4: arg.h4, h5: arg.h5, h6: Lib_Syntax_RApp(Lib_Common_MkFC(arg.h7.h1.h3.h3.h0.h0, Lib_Common_Prelude_Add$20Lib_Common_Bounds$2C_$2B_(arg.h7.h1.h3.h3.h0.h1, _sc$$5.h1)), Lib_Syntax_RVar(arg.h7.h1.h3.h3.h0, arg.h7.h1.h3.h3.h1), arg.h6, 1), h7: arg.h7.h2 }; break; } } break; } default: return { tag: 0, h0: Prelude__$2C_(null, null, arg.h6, arg.h7) }; } break; default: return { tag: 0, h0: Prelude__$2C_(null, null, arg.h6, arg.h7) }; } break; default: return { tag: 0, h0: Prelude__$2C_(null, null, arg.h6, arg.h7) }; } }; const Lib_Parser_pratt_projectHead_runProject_runRule_runPrefix = ( _, _1, _2, _3, _4, _5, _6, _7, _8, _$$9, _$$10, _$$11 ) => { switch (_$$10.tag) { case 0: { const sc$$14 = Data_SortedMap_lookupMap$27(null, null, _$$10.h1, _); switch (sc$$14.tag) { case 0: switch (sc$$14.h1.h3) { case 0: return Lib_Parser_pratt_projectHead_runProject_runRule(_, _1, _2, _3, _4, _5, _6, _7, sc$$14.h1.h1, sc$$14.h1.h2, _$$9, sc$$14.h1.h4, Lib_Syntax_RVar(_$$10.h0, sc$$14.h1.h0), _$$11); default: return Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Prelude__$2C_(null, null, _3, _$$11)); } break; default: return Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Prelude__$2C_(null, null, _3, _$$11)); } break; } default: return Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Prelude__$2C_(null, null, _$$10, _$$11)); } }; const Lib_Syntax_RUpdateRec = ( h0, h1, h2 ) => ({ tag: 15, h0: h0, h1: h1, h2: h2 }); const Lib_Syntax_ModifyField = ( h0, h1, h2 ) => ({ tag: 1, h0: h0, h1: h1, h2: h2 }); @@ -919,7 +923,7 @@ const Prelude_strIndex = (s, ix) => s[ix]; const Lib_Syntax_RLit = ( h0, h1 ) => ({ tag: 7, h0: h0, h1: h1 }); const Lib_Parser_charLit = Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_Impl_getPos, ( fc ) => (Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_Impl_indented(null, Lib_Parser_Impl_token$27(5)), ( v ) => (Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Lib_Syntax_RLit(fc, Lib_Types_LChar(Prelude_strIndex(v, 0)))))))); const Lib_Parser_stringLit = Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_Impl_getPos, ( fc ) => (Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_Impl_indented(null, Lib_Parser_Impl_token$27(6)), ( t ) => (Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Lib_Syntax_RLit(fc, Lib_Types_LString(t))))))); -const Lib_Parser_interpString_append = ( _, _$$1, _$$2 ) => { const fc = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$1); return Lib_Syntax_RApp(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$1), Lib_Syntax_RApp(fc, Lib_Syntax_RVar(fc, "_++_"), _$$1, 1), _$$2, 1); }; +const Lib_Parser_interpString_append = ( _, _$$1, _$$2 ) => { const fc = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$1); const _sc$$0 = Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Raw$2CgetFC(_$$2); return Lib_Syntax_RApp(Lib_Common_MkFC(fc.h0, Lib_Common_Prelude_Add$20Lib_Common_Bounds$2C_$2B_(fc.h1, _sc$$0.h1)), Lib_Syntax_RApp(fc, Lib_Syntax_RVar(fc, "_++_"), _$$1, 1), _$$2, 1); }; const Lib_Parser_interp = Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_Impl_indented(null, Lib_Parser_Impl_token$27(19)), ( _ ) => (Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_term, ( tm ) => (Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_Impl_indented(null, Lib_Parser_Impl_token$27(20)), ( _1 ) => (Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, tm))))))); const Lib_Parser_interpString = Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_Impl_Prelude_Functor$20Lib_Parser_Impl_Parser$2Cmap(null, null, ( _$$3 ) => (0), Lib_Parser_Impl_indented(null, Lib_Parser_Impl_token$27(17))), ( _ ) => (Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_term, ( part ) => (Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_Impl_many(null, Lib_Parser_Impl_Prelude_Alternative$20Lib_Parser_Impl_Parser$2C_$3C$7C$3E_(null, Lib_Parser_stringLit, Lib_Parser_interp)), ( parts ) => (Lib_Parser_Impl_Prelude_Monad$20Lib_Parser_Impl_Parser$2Cbind(null, null, Lib_Parser_Impl_Prelude_Functor$20Lib_Parser_Impl_Parser$2Cmap(null, null, ( _$$3 ) => (0), Lib_Parser_Impl_indented(null, Lib_Parser_Impl_token$27(18))), ( _1 ) => (Lib_Parser_Impl_Prelude_Applicative$20Lib_Parser_Impl_Parser$2Creturn(null, Prelude_foldl(null, null, ( eta ) => (( eta1 ) => (Lib_Parser_interpString_append(null, eta, eta1))), part, parts)))))))))); const Prelude_stringToInt = (s) => { diff --git a/newt-vscode/src/extension.ts b/newt-vscode/src/extension.ts index 355f604..b87aae8 100644 --- a/newt-vscode/src/extension.ts +++ b/newt-vscode/src/extension.ts @@ -40,7 +40,6 @@ export function activate(context: vscode.ExtensionContext) { const lineText = document.lineAt(position.line).text; const start = Math.max(0, position.character - 10); const snippet = lineText.slice(start, position.character); - console.log(`change '${text}' snippet ${snippet}`); const m = snippet.match(/(\\[^ ]+)$/); if (m) { const cand = m[0]; @@ -282,6 +281,49 @@ export function activate(context: vscode.ExtensionContext) { if (document.fileName.endsWith(".newt")) checkDocument(document); context.subscriptions.push(diagnosticCollection); + context.subscriptions.push( + vscode.languages.registerCodeActionsProvider( + { language: "newt" }, + { + provideCodeActions(document, range, context, token) { + const actions: vscode.CodeAction[] = []; + for (const diagnostic of context.diagnostics) { + let {message,range} = diagnostic + let m = diagnostic.message.match(/missing cases: (.*)/); + if (m) { + // A lot of this logic would also apply to case split. + let cons = m[1].split(', '); + const line = diagnostic.range.start.line; + const lineText = document.lineAt(line).text; + let m2 = lineText.match(/(.*=>?)/); + if (!m2) continue; + let s = range.start.character; + let e = range.end.character; + let a = lineText.slice(0,s); + let b = lineText.slice(e,m2[0].length); + let parens = a.endsWith('(') && b.startsWith(')'); + let lines = cons.map(con => + !parens && con.includes('_') + ? `${a}(${con})${b} ?` + : `${a}${con}${b} ?`); + const fix = new vscode.CodeAction( + "Add missing cases", + vscode.CodeActionKind.QuickFix + ); + fix.edit = new vscode.WorkspaceEdit(); + // TODO - we should skip over subsequent lines that are indented more than the current. + const insertPos = new vscode.Position(line + 1, 0); + fix.edit.insert(document.uri, insertPos, lines.join('\n') + '\n'); + fix.diagnostics = [diagnostic]; + fix.isPreferred = true; + actions.push(fix); + } + } + return actions; + } + } + ) + ); } export function deactivate() {} diff --git a/src/Lib/Common.newt b/src/Lib/Common.newt index bd1be71..bca886a 100644 --- a/src/Lib/Common.newt +++ b/src/Lib/Common.newt @@ -14,7 +14,10 @@ record Bounds where -- FIXME we should handle overlap and out of order.. instance Add Bounds where - a + b = MkBounds a.startLine a.startCol b.endLine b.endCol + a + b = + let a' = if a.startLine < b.startLine || a.startLine == b.startLine && a.startCol < b.startCol then a else b + b' = if a.endLine < b.endLine || a.endLine == b.endLine && a.endCol < b.endCol then b else a + in MkBounds a'.startLine a'.startCol b'.endLine b'.endCol instance Eq Bounds where (MkBounds sl sc el ec) == (MkBounds sl' sc' el' ec') = @@ -103,6 +106,9 @@ record FC where bnds : Bounds +instance Add FC where + MkFC fn a + MkFC _ b = MkFC fn (a + b) + instance ToJSON FC where toJson (MkFC file (MkBounds line col endline endcol)) = JsonObj (("file", toJson file) :: ("line", toJson line) :: ("col", toJson col) :: ("endline", toJson endline) :: ("endcol", toJson endcol):: Nil) @@ -132,6 +138,9 @@ emptyFC' fn = MkFC fn (MkBounds 0 0 0 0) data QName : U where QN : List String -> String -> QName +.baseName : QName → String +(QN _ name).baseName = name + instance Eq QName where -- `if` gets us short circuit behavior, idris has a lazy `&&` QN ns n == QN ns' n' = if n == n' then ns == ns' else False @@ -159,7 +168,8 @@ showError src (E fc msg) = "ERROR at \{show fc}: \{msg}\n" ++ go 0 (lines src) go l Nil = "" go l (x :: xs) = if l == fcLine fc then - " \{x}\n \{replicate (cast $ fcCol fc) ' '}^\n" + let width = fc.bnds.endCol - fc.bnds.startCol + 1 in + " \{x}\n \{replicate (cast $ fcCol fc) ' '}\{replicate (cast width) '^'}\n" else if fcLine fc - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs else go (l + 1) xs showError src (Postpone fc ix msg) = "ERROR at \{show fc}: Postpone \{show ix} \{msg}\n" ++ go 0 (lines src) diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 8ec84d2..b3d4c81 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -990,7 +990,7 @@ mkPat (tm, icit) = do (Just (MkEntry _ name type (DCon _ _ k str) _)) => do -- TODO check arity, also figure out why we need reverse bpat <- traverse (mkPat) b - pure $ PatCon fc icit name bpat Nothing + pure $ PatCon (getFC tm) icit name bpat Nothing -- This fires when a global is shadowed by a pattern var -- Just _ => error (getFC tm) "\{show nm} is not a data constructor" _ => case b of @@ -1144,9 +1144,27 @@ buildLitCase ctx prob fc scnm scty lit = do buildDefault : Context → Problem → FC → String → List QName → M CaseAlt buildDefault ctx prob fc scnm missing = do let defclauses = filter isDefault prob.clauses - when (length' defclauses == 0) $ \ _ => error fc "missing cases \{show missing} on \{show scnm}" + -- HACK - For missing cases, we leave enough details in the error message to enable + -- the editor to add them + -- We can't do this precisely without a better pretty printer. + when (length' defclauses == 0) $ \ _ => do + missing <- traverse applied missing + error fc "missing cases: \{show missing}" CaseDefault <$> buildTree ctx (MkProb defclauses prob.ty) where + -- apply a dcon to _ for each explicit argument + applied : QName → M String + applied qn = do + top <- getTop + case lookup qn top of + Just (MkEntry _ _ ty (DCon _ _ _ _) _) => pure $ go qn.baseName ty + _ => pure qn.baseName + where + go : String → Tm → String + go acc (Pi _ _ Explicit _ _ t) = go "\{acc} _" t + go acc (Pi _ _ _ _ _ t) = go acc t + go acc _ = acc + isDefault : Clause -> Bool isDefault cl = case find ((_==_ scnm) ∘ fst) cl.cons of Just (_, (PatVar _ _ _)) => True diff --git a/src/Lib/Parser.newt b/src/Lib/Parser.newt index 0085094..9a211f5 100644 --- a/src/Lib/Parser.newt +++ b/src/Lib/Parser.newt @@ -74,7 +74,7 @@ interpString = do append : Raw -> Raw -> Raw append t u = let fc = getFC t in - (RApp (getFC t) (RApp fc (RVar fc "_++_") t Explicit) u Explicit) + (RApp (fc + getFC u) (RApp fc (RVar fc "_++_") t Explicit) u Explicit) intLit : Parser Raw intLit = do @@ -166,19 +166,18 @@ pratt ops prec stop left spine = do case lookupMap' nm ops of Just (MkOp name p fix False rule) => if p < prec then pure (left, spine) - else - runRule p fix stop rule (RApp fc (RVar fc name) left Explicit) rest + else runRule p fix stop rule (RApp (getFC left + fc) (RVar fc name) left Explicit) rest Just _ => fail "expected operator" Nothing => if isPrefixOf "." nm - then pratt ops prec stop (RApp (getFC tm) tm left Explicit) rest - else pratt ops prec stop (RApp (getFC left) left tm Explicit) rest - ((icit, fc, tm) :: rest) => pratt ops prec stop (RApp (getFC left) left tm icit) rest + then pratt ops prec stop (RApp (getFC left + getFC tm) tm left Explicit) rest + else pratt ops prec stop (RApp (getFC left + getFC tm) left tm Explicit) rest + ((icit, fc, tm) :: rest) => pratt ops prec stop (RApp (getFC left + getFC tm) left tm icit) rest where projectHead : Raw -> AppSpine -> (Raw × AppSpine) projectHead t sp@((Explicit, fc', RVar fc nm) :: rest) = if isPrefixOf "." nm - then projectHead (RApp fc (RVar fc nm) t Explicit) rest + then projectHead (RApp (fc + getFC t) (RVar fc nm) t Explicit) rest else (t,sp) projectHead t sp = (t, sp) @@ -188,7 +187,7 @@ pratt ops prec stop left spine = do runProject : AppSpine -> AppSpine runProject (t@(Explicit, fc', tm) :: u@(Explicit, _, RVar fc nm) :: rest) = if isPrefixOf "." nm - then runProject ((Explicit, fc', RApp fc (RVar fc nm) tm Explicit) :: rest) + then runProject ((Explicit, fc', RApp (fc + getFC tm) (RVar fc nm) tm Explicit) :: rest) else (t :: u :: rest) runProject tms = tms @@ -203,7 +202,7 @@ pratt ops prec stop left spine = do case spine of ((_, fc, right) :: rest) => do (right, rest) <- pratt ops pr stop right rest - pratt ops prec stop (RApp (getFC left) left right Explicit) rest + pratt ops prec stop (RApp (getFC left + getFC right) left right Explicit) rest _ => fail "trailing operator" runRule p fix stop (nm :: rule) left spine = do @@ -215,7 +214,7 @@ pratt ops prec stop left spine = do let ((_,fc',RVar fc name) :: rest) = rest | _ => fail "expected \{nm}" if name == nm - then runRule p fix stop rule (RApp (getFC left) left right Explicit) rest + then runRule p fix stop rule (RApp (getFC left + getFC right) left right Explicit) rest else fail "expected \{nm}" -- run any prefix operators @@ -417,7 +416,9 @@ term = do where apply : Raw -> List (FC × Raw) -> Raw apply t Nil = t - apply t ((fc,x) :: xs) = RApp fc t (apply x xs) Explicit + apply t ((fc,x) :: xs) = + let u = apply x xs in + RApp (getFC t + getFC u) t u Explicit varname : Parser String varname = (ident <|> uident <|> keyword "_" *> pure "_")