diff --git a/.gitignore b/.gitignore index 83dd7e9..80b1e7e 100644 --- a/.gitignore +++ b/.gitignore @@ -13,6 +13,8 @@ mkday.py tmp min.js.gz src/Revision.newt +newt.ss +newt.so .calva .clj-kondo .joyride diff --git a/Makefile b/Makefile index 4eedb65..458431f 100644 --- a/Makefile +++ b/Makefile @@ -22,6 +22,12 @@ newt3.js: newt2.js time $(RUNJS) newt2.js src/Main.newt -o newt3.js cmp newt2.js newt3.js +newt.ss: newt.js + $(RUNJS) newt.js src/Main.newt -o newt.ss + +newt.so: newt.ss + chez --script scripts/compile-chez.ss + test: newt.js scripts/test @@ -32,11 +38,11 @@ aoctest: newt.js # Misc # build / install old vscode extension -vscode: - cd newt-vscode && vsce package && code --install-extension *.vsix +# vscode: + # cd newt-vscode && vsce package && code --install-extension *.vsix # build / install new LSP vscode extension -vscode-lsp: +vscode-lsp vscode: lsp cd newt-vscode-lsp && vsce package && code --install-extension *.vsix playground: .PHONY @@ -65,6 +71,7 @@ playground/src/newt.js: lsp.js newt-vscode-lsp/dist/lsp.js: newt-vscode-lsp/src/lsp.ts newt-vscode-lsp/src/newt.js (cd newt-vscode-lsp && node esbuild.js) + chmod +x $@ lsp: newt-vscode-lsp/dist/lsp.js playground/src/newt.js diff --git a/TODO.md b/TODO.md index 85feeff..af7914d 100644 --- a/TODO.md +++ b/TODO.md @@ -1,14 +1,24 @@ ## TODO -- [ ] Use looping for TCO +- [x] Scheme backend +- [ ] Smart encoding of lists (and cons cells?) in scheme +- [ ] Unsolved meta in Lib.Types doesn't print when building newt. + - delete Show Char to test, it does surface in the LSP, we need to dump these when processing dependent modules +- [ ] maybe `let case` instead of `let ()` (which is a little subtle) + - Or simply put a term in there and treat as a variable iff it is lowercase and non-app +- [x] Use looping for TCO - For single functions at least - I think this would be a performance win. I've learned that the slowness on `bun` goes away if I drop the TCO transform. - Doing this manually for `lookupT23` got 3% speedup. + - got 12% speedup overall from this, not doing it for mutual recursion - [ ] Importing Prelude twice should be an error (currently it causes double hints and breaks auto) - [x] For errors in other files, point to the import - [x] Unsolved metas should be errors (user metas are fine) - [x] Better syntax for forward declared data (so we can distinguish from functions) - [ ] maybe allow "Main" module name for any file +- [ ] preserve information on record / class / instance for LSP "document symbols" kind + - We will want some of this for default implementations in class + - It may help avoid reverse-engineering the class when processing implementation - [ ] Put `Def` on `Ref` - It may be Axiom for forward/recursive functions, but it would get us DCon and TCon info without lookup - and may save passing around the Ref2 (+lookup) during Compilation. - [x] Restore "add missing cases" for LSP mode @@ -24,7 +34,7 @@ - [ ] Duplicate data constructors point to `data` - [ ] Allow Qualified names in surface syntax - Don't disambiguate on type for now - - [ ] Could we disambiguate just Data constructors on type? +- [ ] Could we disambiguate just Data constructors on type? - [x] change "in prefix position" and "trailing operator" errors to do sections - [ ] maybe add fat arrows, I keep wanting to type them, `{{...}}` is a little ugly - There may be ambiguity issues at the parsing level, but we don't have typecase, so. diff --git a/aoc2024/Aoc.newt b/aoc2024/Aoc.newt index 691a15c..c00524f 100644 --- a/aoc2024/Aoc.newt +++ b/aoc2024/Aoc.newt @@ -34,3 +34,8 @@ instance Sub Point where -- instance Eq Point where -- (a,b) == (c,d) = a == c && b == d + +-- Doesn't play well with scheme and was removed from prelude, a couple of days depend on it for BigInt +pfunc jsCompare uses (EQ LT GT) : ∀ a. a → a → Ordering := `(_, a, b) => a == b ? Prelude_EQ : a < b ? Prelude_LT : Prelude_GT` +pfunc jsEq uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a == b ? Prelude_True : Prelude_False` + diff --git a/newt-vscode-lsp/esbuild.js b/newt-vscode-lsp/esbuild.js index 7db336b..435bece 100644 --- a/newt-vscode-lsp/esbuild.js +++ b/newt-vscode-lsp/esbuild.js @@ -35,6 +35,9 @@ async function main() { sourcemap: !production, sourcesContent: false, platform: 'node', + banner: { + js: "#!/usr/bin/env node", + }, // outfile: 'dist/extension.js', outdir: 'dist', external: ['vscode'], diff --git a/newt-vscode-lsp/src/lsp.ts b/newt-vscode-lsp/src/lsp.ts index 4e227b7..040a067 100644 --- a/newt-vscode-lsp/src/lsp.ts +++ b/newt-vscode-lsp/src/lsp.ts @@ -1,6 +1,4 @@ /** - * WIP - * * Wraps newt.js (compiled from src/LSP.newt with some tweaks to `export`) with the * vscode LSP server module. */ @@ -119,10 +117,15 @@ connection.onCodeAction(({textDocument, range}) => { }) connection.onDocumentSymbol((params) => { + try { + const uri = params.textDocument.uri; let symbols = LSP_docSymbols(uri); console.log("docs got", symbols) return symbols; + } catch (e) { + console.error('ERROR in onDocumentSymbol', e); + } }) connection.onInitialize((_params: InitializeParams): InitializeResult => ({ diff --git a/prim.ss b/prim.ss new file mode 100644 index 0000000..4e18b1a --- /dev/null +++ b/prim.ss @@ -0,0 +1,97 @@ +;; REVIEW all of this - some of it is IO and needs the IO dance +;; maybe we make a helper? A macro? + +(define $Nil (lambda (nm-0) (vector 0 nm-0))) +(define $Cons (lambda (nm-0 nm-1 nm-2) (vector 1 nm-0 nm-1 nm-2))) +(define $IORes (lambda (nm-1 nm-2) (vector 0 #f nm-1 nm-2))) +(define ($Left x) (vector 0 #f #f x)) +(define ($Right x) (vector 1 #f #f x)) +(define $LT 0) +(define $EQ 1) +(define $GT 2) +(define (Prelude.addString a b) (string-append a b)) +(define (Prelude.addInt a b) (+ a b)) +(define (Prelude.ltInt a b) (< a b)) +(define (Prelude.eqInt a b) (= a b)) +(define (Prelude.ltChar a b) (charstring) +(define (Node.exitFailure _ msg) (raise msg)) +(define (Prelude.primPutStrLn msg) + (lambda (w) + (display msg) + (newline) + ($IORes #f w))) +(define Prelude.chr integer->char) +(define Prelude.ord char->integer) +(define (Prelude.intToNat x) x) +(define (Prelude.natToInt x) x) +(define (Prelude.slen s) (string-length s)) +(define (Prelude.debugStr _ x) (format #f "~s" x)) +;; REVIEW if this works for all of the cases that it is used for +;; maybe they should all go away for specific instances +(define (Prelude.jsShow x) (format #f "~s" x)) +(define (Node.putStr s) (lambda (w) (display s) ($IORes #f w))) +(define (Prelude.mod x y) (mod x y)) +;; REVIEW returns #f for failure +(define Prelude.stringToInt string->number) + +;; coerce scheme list to newt +(define (list->List xs) + (define (go acc xs) + (if (null? xs) acc + (go ($Cons #f (car xs) acc) (cdr xs)))) + (go ($Nil #f) (reverse xs))) + +(define (List->list xs) + (define (go acc xs) + (if (= 0 (vector-ref xs 0)) (reverse acc) + (go (cons (vector-ref xs 2) acc) (vector-ref xs 3)))) + (go '() xs)) + +(define (Prelude.unpack str) (list->List (string->list str))) +(define (Prelude.pack cs) (list->string (List->list cs))) +(define (Prelude.fastConcat strings) (apply string-append (List->list strings))) + +(define (Prelude.isPrefixOf pfx str) + (string=? pfx (substring str 0 (string-length pfx)))) +;; Only used by getArgs(define Prelude.arrayToList #f) +;; fastConcat uses it in js +(define Prelude.listToArray #f) +(define (Node.readFile fn) + (lambda (w) + (guard (x [else ($IORes ($Left (if (condition? x) + ; (condition-message x) + (with-output-to-string (lambda() (display-condition x))) + "Error")) w)]) + ($IORes ($Right (call-with-input-file fn get-string-all)) w)))) +(define (Node.writeFile fn content) + (lambda (w) + (guard (x [else ($IORes ($Left (if (condition? x) + ; (condition-message x) + (with-output-to-string (lambda() (display-condition x))) + "Error")) w)]) + (with-output-to-file fn + (lambda () (display content)) + 'replace) + ($IORes ($Right #f) w)))) +(define Prelude.strIndex string-ref) +(define (Data.IORef.primNewIORef _ a) (lambda (w) ($IORes (box a) w))) +(define (Data.IORef.primReadIORef _ ref) (lambda (w) ($IORes (unbox ref) w))) +;; Actually should return unit.. +(define (Data.IORef.primWriteIORef _ ref a) (lambda (w) ($IORes (set-box! ref a) w))) +(define (Node.readLine w) + ($IORes ($Right (get-line (current-input-port))) w)) +(define (Prelude.subInt a b) (- a b)) +(define (Prelude.jsEq _ a b) (= a b)) +(define (Prelude.divInt a b) (fx/ a b)) +(define (Prelude.fatalError _ msg) (raise msg)) +(define (Prelude.isSuffixOf sfx s) + (let ((n (string-length sfx)) + (m (string-length s))) + (if (<= n m) + (string=? sfx (substring s (- m n) m)) + #f))) +(define (Node.getArgs w) ($IORes (list->List (command-line)) w)) diff --git a/scripts/compile-chez.ss b/scripts/compile-chez.ss new file mode 100644 index 0000000..9861f67 --- /dev/null +++ b/scripts/compile-chez.ss @@ -0,0 +1 @@ +(parameterize ([optimize-level 3]) (compile-program "newt.ss")) diff --git a/src/Data/List1.newt b/src/Data/List1.newt index a42ab28..d7598f3 100644 --- a/src/Data/List1.newt +++ b/src/Data/List1.newt @@ -9,8 +9,8 @@ record List1 a where head1 : a tail1 : List a -split1 : String → String → List1 String -split1 str by = case split str by of +splitBy1 : String → Char → List1 String +splitBy1 str by = case splitBy str by of Nil => str ::: Nil x :: xs => x ::: xs @@ -22,6 +22,6 @@ unsnoc {a} (x ::: xs) = go x xs go x (y :: ys) = let (as, a) = go y ys in (x :: as, a) splitFileName : String → String × String -splitFileName fn = case split1 fn "." of +splitFileName fn = case splitBy1 fn '.' of part ::: Nil => (part, "") xs => mapFst (joinBy ".") $ unsnoc xs diff --git a/src/Data/SnocList.newt b/src/Data/SnocList.newt index 5afcfd8..f6e7f3d 100644 --- a/src/Data/SnocList.newt +++ b/src/Data/SnocList.newt @@ -9,6 +9,13 @@ snoclen {a} xs = go xs Z go Lin acc = acc go (xs :< x) acc = go xs (S acc) +snoclen' : ∀ a. SnocList a → Int +snoclen' {a} xs = go xs 0 + where + go : SnocList a → Int → Int + go Lin acc = acc + go (xs :< x) acc = go xs (1 + acc) + snocelem : ∀ a. {{Eq a}} → a → SnocList a → Bool snocelem a Lin = False snocelem a (xs :< x) = if a == x then True else snocelem a xs diff --git a/src/LSP.newt b/src/LSP.newt index 75b0769..1fe223f 100644 --- a/src/LSP.newt +++ b/src/LSP.newt @@ -16,7 +16,7 @@ import Commands import Lib.ProcessDecl import Lib.Prettier import Lib.Error -import Lib.Compile +import Lib.CompileJS pfunc js_castArray : Array JSObject → JSObject := `x => x` pfunc js_castInt : Int → JSObject := `x => x` @@ -291,6 +291,4 @@ compileJS fn = unsafePerformIO $ do modifyIORef state [ topContext := top ] pure $ js_castStr src - - #export updateFile checkFile hoverInfo codeActionInfo compileJS docSymbols diff --git a/src/Lib/Common.newt b/src/Lib/Common.newt index 5e09d33..f8bb226 100644 --- a/src/Lib/Common.newt +++ b/src/Lib/Common.newt @@ -55,6 +55,12 @@ toHex : Int -> List Char toHex 0 = Nil toHex v = snoc (toHex (div v 16)) (hexDigit v) +padding : Int → Char → String +padding n ch = go n Nil + where + go : Int → List Char → String + go 0 chs = pack chs + go k chs = go (k - 1) (ch :: chs) quoteString : String -> String quoteString str = pack $ encode (unpack str) (Lin :< '"') diff --git a/src/Lib/CompileExp.newt b/src/Lib/CompileExp.newt index a21f7ef..0c501e8 100644 --- a/src/Lib/CompileExp.newt +++ b/src/Lib/CompileExp.newt @@ -57,18 +57,6 @@ lamArity : Tm -> List Quant lamArity (Lam _ _ _ quant t) = quant :: (lamArity t) lamArity _ = Nil --- It would be nice to be able to declare these -compilePrimOp : String → List CExp → Maybe CExp -compilePrimOp "Prelude.addString" (x :: y :: Nil) = Just (CPrimOp "+" x y) -compilePrimOp "Prelude.addInt" (x :: y :: Nil) = Just (CPrimOp "+" x y) -compilePrimOp "Prelude.mulInt" (x :: y :: Nil) = Just (CPrimOp "*" x y) -compilePrimOp "Prelude.subInt" (x :: y :: Nil) = Just (CPrimOp "-" x y) -compilePrimOp "Prelude._&&_" (x :: y :: Nil) = Just (CPrimOp "&&" x y) -compilePrimOp "Prelude._||_" (x :: y :: Nil) = Just (CPrimOp "||" x y) --- Assumes Bool is in the right order! -compilePrimOp "Prelude.jsEq" (_ :: x :: y :: Nil) = Just (CPrimOp "==" x y) -compilePrimOp "Prelude.divInt" (x :: y :: Nil) = Just (CPrimOp "|" (CPrimOp "/" x y) (CLit $ LInt 0)) -compilePrimOp _ _ = Nothing -- This is how much we want to curry at top level -- leading lambda Arity is used for function defs and metas @@ -80,11 +68,11 @@ arityForName fc nm = do Nothing => error fc "Name \{show nm} not in scope" (Just Axiom) => pure Nil (Just (PrimOp _)) => pure $ Many :: Many :: Nil - (Just (TCon arity strs)) => pure $ replicate' (cast arity) Many + (Just (TCon arity strs)) => pure $ replicate (cast arity) Many (Just (DCon _ _ arity str)) => pure arity (Just (Fn t)) => pure $ lamArity t - (Just (PrimTCon arity)) => pure $ replicate' (cast arity) Many - (Just (PrimFn t arity used)) => pure $ replicate' arity Many + (Just (PrimTCon arity)) => pure $ replicate (cast arity) Many + (Just (PrimFn t arity used)) => pure $ replicate arity Many where @@ -147,8 +135,6 @@ compileTerm tm@(App _ _ _) = case funArgs tm of defs <- getRef Defs args' <- traverse compileTerm args arity <- arityForName fc nm - let (Nothing) = compilePrimOp (show nm) args' - | Just cexp => pure cexp case lookupMap' nm defs : Maybe Def of Just (DCon _ SuccCon _ _) => applySucc args' _ => apply nm args' arity @@ -277,7 +263,7 @@ defToCExp (qn, (PrimOp _)) = (_,_ qn) <$> compilePop qn defToCExp (qn, DCon ix info arity _) = pure (qn, compileDCon ix qn info arity) -- We're not using these are runtime at the moment, no typecase -- we need to sort out tag number if we do typecase -defToCExp (qn, TCon arity conNames) = pure (qn, compileDCon Z qn NormalCon (replicate' (cast arity) Many)) -defToCExp (qn, PrimTCon arity) = pure (qn, compileDCon Z qn NormalCon (replicate' (cast arity) Many)) +defToCExp (qn, TCon arity conNames) = pure (qn, compileDCon Z qn NormalCon (replicate (cast arity) Many)) +defToCExp (qn, PrimTCon arity) = pure (qn, compileDCon Z qn NormalCon (replicate (cast arity) Many)) defToCExp (qn, PrimFn src _ deps) = pure (qn, CRaw src deps) defToCExp (qn, Fn tm) = (_,_ qn) <$> compileFun tm diff --git a/src/Lib/Compile.newt b/src/Lib/CompileJS.newt similarity index 92% rename from src/Lib/Compile.newt rename to src/Lib/CompileJS.newt index 52a8e90..0b59dc6 100644 --- a/src/Lib/Compile.newt +++ b/src/Lib/CompileJS.newt @@ -1,7 +1,4 @@ --- TODO Audit how much "outside" stuff could pile up in the continuation. (How much might be repeated in case branches.) --- TODO consider inlining constructors here (a future inline process might do this anyway). --- TODO consider not emitting null in `LitObject` (after inlining constructors) -module Lib.Compile +module Lib.CompileJS import Prelude import Lib.Common @@ -147,6 +144,25 @@ getEnv ix env = case getAt' ix env of Just e => e Nothing => fatalError "Bad bounds \{show ix}" +-- It would be nice to be able to declare these +compilePrimOp : String → List CExp → Maybe CExp +compilePrimOp "Prelude.addString" (x :: y :: Nil) = Just (CPrimOp "+" x y) +compilePrimOp "Prelude.addInt" (x :: y :: Nil) = Just (CPrimOp "+" x y) +compilePrimOp "Prelude.mulInt" (x :: y :: Nil) = Just (CPrimOp "*" x y) +compilePrimOp "Prelude.subInt" (x :: y :: Nil) = Just (CPrimOp "-" x y) +compilePrimOp "Prelude._&&_" (x :: y :: Nil) = Just (CPrimOp "&&" x y) +compilePrimOp "Prelude._||_" (x :: y :: Nil) = Just (CPrimOp "||" x y) +-- Assumes Bool is in the right order! +compilePrimOp "Prelude.jsEq" (_ :: x :: y :: Nil) = Just (CPrimOp "==" x y) +compilePrimOp "Prelude.eqChar" (_ :: x :: y :: Nil) = Just (CPrimOp "==" x y) +compilePrimOp "Prelude.ltChar" (_ :: x :: y :: Nil) = Just (CPrimOp "<" x y) +compilePrimOp "Prelude.eqInt" (_ :: x :: y :: Nil) = Just (CPrimOp "==" x y) +compilePrimOp "Prelude.ltInt" (_ :: x :: y :: Nil) = Just (CPrimOp "<" x y) +compilePrimOp "Prelude.eqString" (_ :: x :: y :: Nil) = Just (CPrimOp "==" x y) +compilePrimOp "Prelude.ltString" (_ :: x :: y :: Nil) = Just (CPrimOp "<" x y) +compilePrimOp "Prelude.divInt" (x :: y :: Nil) = Just (CPrimOp "|" (CPrimOp "/" x y) (CLit $ LInt 0)) +compilePrimOp _ _ = Nothing + -- This is inspired by A-normalization, look into the continuation monad -- There is an index on JSStmt, adopted from Stefan Hoeck's code. -- @@ -224,7 +240,10 @@ termToJS {e} env (CLoop args quants) f = runArgs (reverse env.jsenv) args quants runArgs (JUndefined :: rest) (arg :: args) (q :: qs) = runArgs rest args qs runArgs (wat :: rest) (arg :: args) (q :: qs) = fatalError "bad env for quant \{show q}" runArgs a b c = fatalError "FALLBACK \{show $ length' a} \{show $ length' b} \{show $ length' c}" -termToJS env (CAppRef nm args quants) f = termToJS env (CRef nm) (\ t' => (argsToJS env t' args quants Lin f)) +termToJS env (CAppRef nm args quants) f = + case compilePrimOp (show nm) args of + Just cexp => termToJS env cexp f + Nothing => termToJS env (CRef nm) (\ t' => (argsToJS env t' args quants Lin f)) where etaExpand : JSEnv -> List Quant -> SnocList JSExp -> JSExp -> JSExp etaExpand env Nil args tm = Apply tm (args <>> Nil) @@ -261,11 +280,16 @@ termToJS {e} env (CCase t alts) f = -- TODO with inlining, we hit cases where the let gets pulled forward more than once -- two cases as separate args, se we need actual unique names. For now, we're calling -- incr when processing App, as a stopgap, we probably need a fresh names state monad + -- also TODO find out when the case builder pulls out sc$ for us and when we do + -- _sc here. It seems like nm doesn't get used in the CDefAlt case. + -- possibly from inlining? + -- Lib.Parser.pratt has two (hence the incr) + -- and record updates hit _sc$ let nm = "_sc$\{show env.depth}" -- increment the bit that goes into the name env' = incr env in if simpleJSExp t' - then (maybeCaseStmt env' t' alts) + then (maybeCaseStmt env t' alts) else JSnoc (JConst nm t') (maybeCaseStmt env' (Var nm) alts) where tertiary : JSExp → JSStmt e → JSStmt e → Cont e → JSStmt e @@ -290,15 +314,18 @@ termToJS {e} env (CCase t alts) f = maybeCaseStmt env sc alts@(CLitAlt _ _ :: _) = (JCase sc (map (termToJSAlt env sc) alts)) maybeCaseStmt env sc alts = case alts of + -- Bool alt becomes tertiary operator CLitAlt (LBool b) rhs :: alt :: Nil => let t' = termToJS env rhs f e' = termToJS env (getBody alt) f in if b then tertiary sc t' e' f else tertiary sc e' t' f + -- two branch alt becomes tertiary operator CConAlt ix name info args t :: alt :: Nil => let cond = (JPrimOp "==" (Dot sc "tag") (LitInt $ cast ix)) t' = termToJS (conAltEnv sc 0 env args) t f u' = termToJS (conAltEnv sc 0 env $ getArgs alt) (getBody alt) f in tertiary cond t' u' f + -- fall back to switch statement alts => JCase (Dot sc "tag") (map (termToJSAlt env sc) alts) jsKeywords : List String diff --git a/src/Lib/CompileScheme.newt b/src/Lib/CompileScheme.newt new file mode 100644 index 0000000..820beee --- /dev/null +++ b/src/Lib/CompileScheme.newt @@ -0,0 +1,338 @@ +module Lib.CompileScheme + +import Prelude +import Lib.Common +import Lib.Types +import Lib.Eval +import Lib.Prettier +import Lib.CompileExp +import Lib.TopContext +import Lib.LiftWhere +import Lib.LiftLambda +import Lib.TCO +import Lib.Ref2 +import Lib.Erasure +import Data.String +import Data.Int +import Data.SortedMap +import Data.IORef +import Data.SnocList + +SCEnv : U +SCEnv = List String + +getEnv : Int → SCEnv → String +getEnv ix env = case getAt' ix env of + Just e => e + Nothing => fatalError "Bad bounds \{show ix}" + +scbind : String → SCEnv → (String × SCEnv) +scbind nm env = let + x = length' env + nm' = "nm-\{show x}" + in (nm', nm' :: env) + +-- TODO +scmKeywords : List String +scmKeywords = "lambda" :: Nil + +scmIdent : String → String +scmIdent id = if elem id scmKeywords then "$" ++ id else pack $ fix (unpack id) + where + fix : List Char -> List Char + fix Nil = Nil + fix (x :: xs) = + if isAlphaNum x || x == '_' || x == '.' then + x :: fix xs + -- make qualified names more readable + else if x == ',' then '_' :: fix xs + else if x == ' ' then '_' :: fix xs + else if x == '$' then + '$' :: '$' :: fix xs + else + '$' :: (toHex (cast x)) ++ fix xs + + +scmLit : Literal → String +scmLit (LString str) = quoteString str +scmLit (LInt n) = show n +scmLit (LChar c) = pack $ '#' :: '\\' :: c :: Nil -- FIXME +scmLit (LBool b) = ite b "#t" "#f" + +scmName : QName → String +scmName qn = scmIdent $ show qn + +cexpToScm : SCEnv → CExp → String + +withVar : SCEnv → CExp → (String → String) → String +-- withVar env (CBnd _) f = ? +-- withVar env (CLit _) f = ? +withVar env t f = let nm = "wv$\{show $ length' env}" + in "(let ((\{nm} \{cexpToScm env t})) \{f nm})" + +cexpToScm env (CBnd n) = getEnv n env +cexpToScm env (CLam nm t) = case scbind nm env of + (nm', env') => "(lambda (\{nm'}) \{cexpToScm env' t})" +cexpToScm env (CFun args body) = case bindAll args Lin env of + (nms,env') => "(lambda (\{joinBy " " nms}) \{cexpToScm env' body})" + where + bindAll : List (Quant × String) → SnocList String → SCEnv → List String × SCEnv + bindAll Nil acc env = (acc <>> Nil, env) + bindAll ((_,nm) :: rest) acc env = case scbind nm env of + (nm', env') => bindAll rest (acc :< nm') env' +cexpToScm env (CApp t u) = "(\{cexpToScm env t} \{cexpToScm env u})" +cexpToScm env (CAppRef nm args Nil) = go (scmName nm) $ map (cexpToScm env) args + where + go : String → List String → String + go acc Nil = acc + go acc (arg :: args) = go "(\{acc} \{arg})" args +-- If we're short, we need to eta expand +cexpToScm env (CAppRef nm args quants) = + go env "(\{scmName nm}" (map (cexpToScm env) args) quants + where + -- here `acc` is always missing a closing paren + go : SCEnv → String → List String → List Quant → String + go env acc Nil Nil = acc ++ ")" + -- extra args are applied + go env acc (arg :: args) Nil = go env "(\{acc}) \{arg}" args Nil + -- missing args get eta expanded + go env acc Nil (q :: qs) = case scbind "_" env of + (nm, env') => let acc = "\{acc} \{nm}" in "(lambda (\{nm}) \{go env' acc Nil qs})" + -- TODO / REVIEW Only for Many? + go env acc (arg :: args) (q :: qs) = go env "\{acc} \{arg}" args qs + -- go env acc (arg :: args) (q :: qs) = go env acc args qs +-- so... we're not giving scrutinee a deBruijn index, but we may +-- need to let it so we can pull data off for the CConAlt +cexpToScm env (CCase sc alts) = do + -- assign sc, might need to do more to make the name unique, we only + -- get one of these per env at the moment + -- Not vector-ref for CLitAlt... + withVar env sc $ \ nm => doCase nm alts + where + -- add a bunch of lets then do body + conAlt : SCEnv → String → SnocList String → List String → CExp → String + conAlt env nm lets Nil body = "(let (\{joinBy " " (lets <>> Nil)}) \{cexpToScm env body})" + -- TODO let `vector-ref nm ..`` vs `#f` (erased) in env for erased fields + conAlt env nm lets (arg :: args) body = case scbind arg env of + (arg', env') => let ix = 1 + snoclen' lets + in conAlt env' nm (lets :< "(\{arg'} (vector-ref \{nm} \{show ix}))") args body + + doAlt : String → CAlt → String + doAlt nm (CConAlt tag cname _ args body) = "((\{show tag}) \{conAlt env nm Lin args body})" + doAlt nm (CDefAlt body) = "(else \{cexpToScm env body})" + doAlt nm (CLitAlt lit body) = "((\{scmLit lit}) \{cexpToScm env body})" + + doCase : String → List CAlt → String + doCase nm alts@(CLitAlt _ _ :: _) = "(case \{nm} \{joinBy " " $ map (doAlt nm) alts})" + doCase nm alts = "(case (vector-ref \{cexpToScm env sc} 0) \{joinBy " " $ map (doAlt nm) alts})" + +cexpToScm env (CRef nm) = scmName nm +cexpToScm env (CMeta _) = fatalError "meta in code gen" +cexpToScm env (CLit lit) = scmLit lit +cexpToScm env (CLet nm t u) = + let (nm',env') = scbind nm env in + "(let ((\{nm'} \{cexpToScm env t})) \{cexpToScm env' u})" +cexpToScm env (CLetRec nm t u) = + let (nm',env') = scbind nm env in + "(let ((\{nm'} \{cexpToScm env' t})) \{cexpToScm env' u})" +cexpToScm env (CLetLoop _ _) = fatalError "CLetLoop in scheme codegen" +cexpToScm env (CLoop _ _) = fatalError "CLoop in scheme codegen" +cexpToScm env CErased = "#f" +cexpToScm env (CConstr tag nm args quants) = + -- FIXME need to deal with quants + let args' = map (cexpToScm env) args in + "(vector \{show tag} \{joinBy " " args'})" +-- TODO +cexpToScm env (CRaw _ _) = "CRaw" +-- TODO We still have a couple of these in CompileExp, for the magic Nat +cexpToScm env (CPrimOp op a b) = "(\{op} \{cexpToScm env a} \{cexpToScm env b})" + + +-- Collect the QNames used in a term +getNames : Tm -> List QName -> List QName +getNames (Ref x nm) acc = nm :: acc +getNames (Lam x str _ _ t) acc = getNames t acc +getNames (App x t u) acc = getNames u $ getNames t acc +getNames (Pi x str icit y t u) acc = getNames u $ getNames t $ QN primNS "PiType" :: acc +getNames (Let x str t u) acc = getNames u $ getNames t acc +getNames (LetRec x str _ t u) acc = getNames u $ getNames t acc +getNames (Case x t alts) acc = getNames t $ foldl getAltNames acc alts + where + getAltNames : List QName -> CaseAlt -> List QName + getAltNames acc (CaseDefault t) = getNames t acc + getAltNames acc (CaseCons name args t) = name :: getNames t acc + getAltNames acc (CaseLit lit t) = getNames t acc +getNames _ acc = acc + +-- returns a QName -> Def of in-use entries +-- This will be what we work on for optimization passes +getEntries : SortedMap QName Def → QName → M (SortedMap QName Def) +getEntries acc name = do + top <- getTop + case lookup name top of + Nothing => do + putStrLn "bad name \{show name}" + pure acc + Just (MkEntry _ name type def@(Fn exp) _) => case lookupMap' name acc of + Just _ => pure acc + Nothing => do + top <- getTop + exp <- zonk top 0 Nil exp + let acc = updateMap name (Fn exp) acc + foldlM getEntries acc $ getNames exp Nil + Just (MkEntry _ name type def@(PrimFn _ _ used) _) => + let acc = updateMap name def acc in + foldlM getEntries acc used + Just entry => pure $ updateMap name entry.def acc + +/- + +## Sort names by dependencies + +This code is _way too subtle. The problem goes away if I wrap `() =>` around 0-ary top level functions. But I'm +stubborn, so I'm giving it a try. Changing codegen may repeatedly break this and require switching to `() =>`. + +The idea here is to get a list of names to emit in order of dependencies. But top level 0-ary functions can reference +and call names at startup. They can't reference something that hasn't been declared yet and can't call something that +hasn't been defined. + +As an example, a recursive show instance: +- References the `show` function +- `show` function references the instance under a lambda (not inlining this yet) +- We hit the bare function first, it depends on the instance (because of recursion), which depends on the + function, but loop prevention cuts. + +We have main at the top, it is called so we visit it deep. We do a depth-first traversal, but will distinguish whether +we're visiting shallow or deep. We're trying to avoid hitting issues with indirect circular references. + +- Anything we visit deep, we ensure is visited shallow first +- Shallow doesn't go into function bodies, but we do go into lambdas +- Anything invoked with arguments while shallow is visited deep, anything referenced or partially applied is still shallow. +- We keep track of both shallow and deep visits in our accumuulator +- Shallow represents the declaration, so we filter to those at the end + +TODO this could be made faster by keeping a map of the done information +REVIEW could I avoid most of this by using `function` instead of arrow functions? + +-/ + +sortedNames : SortedMap QName CExp → List QName → List QName +sortedNames defs names = + map snd $ filter (not ∘ fst) $ foldl (go Nil) Nil $ map (True,) names + where + getBody : CAlt → CExp + getBody (CConAlt _ _ _ _ t) = t + getBody (CLitAlt _ t) = t + getBody (CDefAlt t) = t + + -- deep if this qn is being applied to something + getNames : (deep : Bool) → List (Bool × QName) → CExp → List (Bool × QName) + -- liftIO calls a lambda statically + getNames deep acc (CLam _ t) = getNames deep acc t + getNames deep acc (CLetLoop _ t) = getNames deep acc t + -- top level 0-ary function, doesn't happen + getNames deep acc (CFun _ t) = if deep then getNames deep acc t else acc + -- REVIEW - True or deep? + getNames deep acc (CLoop args qs) = foldl (getNames True) acc args + getNames deep acc (CAppRef nm args qs) = + if length' args == length' qs + then case args of + Nil => (True, nm) :: acc + ts => foldl (getNames True) ((True, nm) :: acc) ts + else + foldl (getNames deep) ((deep, nm) :: acc) args + -- TODO look at which cases generate CApp + getNames deep acc (CApp t u) = getNames True (getNames deep acc u) t + getNames deep acc (CCase t alts) = foldl (getNames deep) acc $ t :: map getBody alts + -- we're not calling it + getNames deep acc (CRef qn) = (deep, qn) :: acc + getNames deep acc (CLet _ t u) = getNames deep (getNames deep acc t) u + getNames deep acc (CLetRec _ t u) = getNames deep (getNames deep acc t) u + getNames deep acc (CConstr _ _ ts _) = foldl (getNames deep) acc ts + -- if the CRaw is called, then the deps are called + getNames deep acc (CRaw _ deps) = acc -- map (_,_ deep) deps ++ acc + -- wrote these out so I get an error when I add a new constructor + getNames deep acc (CLit _) = acc + getNames deep acc (CMeta _) = acc + getNames deep acc (CBnd _) = acc + getNames deep acc CErased = acc + getNames deep acc (CPrimOp op t u) = getNames deep (getNames deep acc t) u + + -- recurse on all dependencies, pushing onto acc + go : List (Bool × QName) → List (Bool × QName) → (Bool × QName) → List (Bool × QName) + -- Need to force shallow if we're doing deep and haven't done shallow. + go loop acc this@(deep, qn) = + -- there is a subtle issue here with an existing (False, qn) vs (True, qn) + let acc = if deep && not (elem (False, qn) acc) && not (elem (False, qn) loop) + then go loop acc (False, qn) + else acc + in if elem this loop + then acc + else if elem this acc then acc + else + case lookupMap' qn defs of + Nothing => acc -- only `bouncer` + Just exp => this :: foldl (go $ this :: loop) acc (getNames deep Nil exp) + +eraseEntries : {{Ref2 Defs St}} → M Unit +eraseEntries = do + defs <- getRef Defs + ignore $ traverse go $ toList defs + where + go : {{Ref2 Defs St}} → (QName × Def) → M Unit + go (qn, Fn tm) = do + tm' <- erase Nil tm Nil + modifyRef Defs $ updateMap qn (Fn tm') + go _ = pure MkUnit + +-- given a initial function, return a dependency-ordered list of javascript source +process : List QName → M (List String) +process names = do + top <- getTop + entries <- foldlM getEntries emptyMap names + + -- Maybe move this dance into liftWhere + ref <- newIORef entries + let foo = MkRef ref -- for the autos below + eraseEntries + liftWhere + entries <- readIORef ref + -- Now working with defs + exprs <- mapM defToCExp $ toList entries + let cexpMap = foldMap const emptyMap exprs + -- not needed for scheme + -- cexpMap <- tailCallOpt cexpMap + -- Not needed for scheme + -- cexpMap <- liftLambda cexpMap + let names = sortedNames cexpMap names + pure $ mapMaybe (go cexpMap) names + where + go : ExpMap → QName → Maybe String + go cexpMap name = do + (qn, cexp) <- lookupMap name cexpMap + case cexp of + CRaw _ _ => Nothing + _ => Just $ "(define \{scmName qn} \{cexpToScm Nil cexp})" + +compileScheme : M (List String) +compileScheme = do + top <- getTop + let exports = getExports Nil $ listValues top.currentMod.modDefs + let mainName = (QN top.currentMod.modName "main") + let main = lookup mainName top + let todo = case main of + Nothing => exports + Just _ => mainName :: exports + defs <- process todo + case lookup mainName top of + Just _ => -- tack on call to main function + let exec = "(\{show mainName} 'world)" + in pure $ "(import (chezscheme))" :: "(include \"prim.ss\")" :: reverse (exec :: defs) + Nothing => pure $ reverse defs + where + getExports : List QName → List TopEntry → List QName + getExports acc Nil = acc + getExports acc ((MkEntry fc name@(QN ns nm) type def eflags) :: rest) = + let acc = if elem Export eflags then name :: acc else acc + in getExports acc rest + diff --git a/src/Lib/Error.newt b/src/Lib/Error.newt index 2efe79f..fc3abf4 100644 --- a/src/Lib/Error.newt +++ b/src/Lib/Error.newt @@ -31,7 +31,7 @@ showError src err = go fc l (x :: xs) = if l == fcLine fc then let width = fc.bnds.endCol - fc.bnds.startCol in - " \{x}\n \{replicate (cast $ fcCol fc) ' '}\{replicate (cast width) '^'}\n" + " \{x}\n \{padding (fcCol fc) ' '}\{padding width '^'}\n" else if fcLine fc - 3 < l then " " ++ x ++ "\n" ++ go fc (l + 1) xs else go fc (l + 1) xs diff --git a/src/Lib/Parser/Impl.newt b/src/Lib/Parser/Impl.newt index 0ebb516..9ac69b5 100644 --- a/src/Lib/Parser/Impl.newt +++ b/src/Lib/Parser/Impl.newt @@ -76,7 +76,7 @@ getOps = P $ \last toks com ops col => OK ops last toks com ops addOp : String -> Int -> Fixity -> Parser Unit addOp nm prec fix = P $ \ last toks com ops col => - let parts = split nm "_" in + let parts = splitBy nm '_' in case parts of "" :: key :: rule => OK MkUnit last toks com (updateMap key (MkOp nm prec fix False rule) ops) key :: rule => OK MkUnit last toks com (updateMap key (MkOp nm prec fix True rule) ops) diff --git a/src/Lib/Prettier.newt b/src/Lib/Prettier.newt index c30dbe2..bb9a409 100644 --- a/src/Lib/Prettier.newt +++ b/src/Lib/Prettier.newt @@ -2,6 +2,7 @@ -- https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf module Lib.Prettier import Prelude +import Lib.Common import Data.Int -- TODO I broke this when I converted from Nat to Int, and we're disabling it @@ -44,7 +45,7 @@ group x = Alt (flatten x) x -- TODO - we can accumulate snoc and cat all at once layout : List Item -> SnocList String -> String layout Nil acc = fastConcat $ acc <>> Nil -layout (LINE k :: x) acc = layout x (acc :< "\n" :< replicate (cast k) ' ') +layout (LINE k :: x) acc = layout x (acc :< "\n" :< padding k ' ') layout (TEXT str :: x) acc = layout x (acc :< str) -- Whether a documents first line fits. diff --git a/src/Lib/ProcessModule.newt b/src/Lib/ProcessModule.newt index 89582d0..3f797bc 100644 --- a/src/Lib/ProcessModule.newt +++ b/src/Lib/ProcessModule.newt @@ -47,7 +47,7 @@ parseDecls fn ops toks@(first :: _) acc = else recover toks importToName : Import → List String -importToName (MkImport fc (_,name)) = split name "." +importToName (MkImport fc (_,name)) = splitBy name '.' importHints : List TopEntry → M Unit importHints Nil = pure MkUnit @@ -69,7 +69,7 @@ processModule importFC repo stk modns = do let (False) = modns == primNS | _ => addPrimitives let freshMC = MC emptyMap Nil 0 CheckAll - let parts = split modns "." + let parts = splitBy modns '.' let fn = joinBy "/" parts ++ ".newt" -- Dummy for initial load/parse @@ -144,6 +144,7 @@ processModule importFC repo stk modns = do -- This has addErrors as a side-effect logMetas $ reverse $ listValues top.currentMod.modMetaCtx.metas + top <- getTop -- print errors (for batch processing case) for_ (reverse top.currentMod.modErrors) $ \ err => putStrLn $ showError src err diff --git a/src/Lib/ReplParser.newt b/src/Lib/ReplParser.newt index 6d132d3..e6fb70d 100644 --- a/src/Lib/ReplParser.newt +++ b/src/Lib/ReplParser.newt @@ -36,7 +36,7 @@ replQN = do ident <- uident rest <- many $ token Projection let name = joinBy "" (ident :: rest) - let (ns,nm) = unsnoc $ split1 name "." + let (ns,nm) = unsnoc $ splitBy1 name '.' pure $ QN (joinBy "." ns) nm data ArgType = ArgNone | ArgString | ArgIdent | ArgOptInt | ArgQName diff --git a/src/Lib/Util.newt b/src/Lib/Util.newt index f962cb0..beb02d3 100644 --- a/src/Lib/Util.newt +++ b/src/Lib/Util.newt @@ -34,7 +34,7 @@ splitTele = go Nil getBaseDir : String → FC → List String → M String getBaseDir fn fc modName = do let path = fst $ splitFileName fn - let dirs = split path "/" + let dirs = splitBy path '/' let (Right base) = baseDir (Lin <>< dirs) (Lin <>< modName) | Left err => error fc err let base = if base == "" then "." else base diff --git a/src/Main.newt b/src/Main.newt index d8a1a6c..8e17371 100644 --- a/src/Main.newt +++ b/src/Main.newt @@ -4,7 +4,8 @@ import Prelude import Data.List1 import Data.SortedMap import Lib.Common -import Lib.Compile +import Lib.CompileJS +import Lib.CompileScheme import Lib.Parser import Lib.Elab import Lib.Util @@ -43,6 +44,14 @@ jsonTopContext = do :: ("type", toJson (render 80 $ pprint Nil type) ) :: Nil) +writeScheme : String → M Unit +writeScheme fn = do + lines <- compileScheme + let src = unlines lines + (Right _) <- liftIO {M} $ writeFile fn src + | Left err => throwError $ E (MkFC fn $ MkBounds 0 0 0 0) err + pure MkUnit + writeSource : String -> M Unit writeSource fn = do docs <- compile @@ -77,7 +86,7 @@ showErrors fn src = do processFile : String -> M Unit processFile fn = do putStrLn "*** Process \{fn}" - let parts = split1 fn "/" + let parts = splitBy1 fn '/' let (dirs,file) = unsnoc parts let dir = if dirs == Nil then "." else joinBy "/" dirs let (name, ext) = splitFileName file @@ -90,7 +99,7 @@ processFile fn = do let (Right ((nameFC, modName), _, _)) = partialParse fn parseModHeader emptyMap toks | Left (err,toks) => throwError err - let modns = split modName "." + let modns = splitBy modName '.' base <- getBaseDir fn nameFC modns invalidateModule modName @@ -201,7 +210,10 @@ main' = do case out of Nothing => pure MkUnit - Just name => writeSource name + Just name => + if isSuffixOf ".ss" name then writeScheme name + else if isSuffixOf ".js" name then writeSource name + else exitFailure "Unknown extension for output file \{show name} - I only know .js and .ss" main : IO Unit main = do diff --git a/src/Prelude.newt b/src/Prelude.newt index 396eaad..43274e2 100644 --- a/src/Prelude.newt +++ b/src/Prelude.newt @@ -265,18 +265,22 @@ instance Concat String where _++_ = addString -pfunc jsEq uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a == b ? Prelude_True : Prelude_False` -pfunc jsLT uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a < b ? Prelude_True : Prelude_False` +pfunc ltInt : Int → Int → Bool := `(a,b) => a < b` +pfunc eqInt : Int → Int → Bool := `(a,b) => a == b` +pfunc ltChar : Char → Char → Bool := `(a,b) => a < b` +pfunc eqChar : Char → Char → Bool := `(a,b) => a == b` +pfunc ltString : String → String → Bool := `(a,b) => a < b` +pfunc eqString : String → String → Bool := `(a,b) => a == b` pfunc jsShow : ∀ a . a → String := `(_,a) => ''+a` instance Eq Int where - a == b = jsEq a b + a == b = eqInt a b instance Eq String where - a == b = jsEq a b + a == b = eqString a b instance Eq Char where - a == b = jsEq a b + a == b = eqChar a b @@ -304,9 +308,6 @@ pfunc arrayToList uses (Nil _::_) : ∀ a. Array a → List a := `(a,arr) => { return rval }` --- for now I'll run this in JS -pfunc lines uses (arrayToList) : String → List String := `(s) => Prelude_arrayToList(null,s.split('\n'))` - pfunc p_strHead : (s : String) → Char := `(s) => s[0]` pfunc p_strTail : (s : String) → String := `(s) => s[0]` @@ -326,11 +327,9 @@ pfunc natToInt : Nat → Int := `(n) => n` pfunc intToNat : Int → Nat := `(n) => n>0?n:0` pfunc fastConcat uses (listToArray) : List String → String := `(xs) => Prelude_listToArray(null, xs).join('')` -pfunc replicate uses (natToInt) : Nat → Char → String := `(n,c) => c.repeat(Prelude_natToInt(n))` --- TODO this should be replicate and the chars thing should have a different name -replicate' : ∀ a. Nat → a → List a -replicate' {a} n x = go n Nil +replicate : ∀ a. Nat → a → List a +replicate {a} n x = go n Nil where go : Nat → List a → List a go Z xs = xs @@ -433,43 +432,23 @@ pfunc pack : List Char → String := `(cs) => { } ` --- FIXME this no longer works with numeric tags --- we could take the best of both worlds and have a debug flag to add extra information --- but also we could derive Show... -pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => { - const go = (obj) => { - if (obj === null) return "_" - if (typeof obj == 'bigint') return ''+obj - if (obj.tag === '_,_') { - let rval = '(' - while (obj?.tag === '_,_') { - rval += go(obj.h2) + ', ' - obj = obj.h3 - } - return rval + go(obj) + ')' - } - if (obj?.tag === '_::_' || obj?.tag === 'Nil') { - let stuff = Prelude_listToArray(null,obj) - return '['+(stuff.map(go).join(', '))+']' - } - if (obj instanceof Array) { - return 'io['+(obj.map(go).join(', '))+']' - } - if (obj?.tag === 'S' || obj?.tag === 'Z') { - return ''+Prelude_natToInt(obj) - } else if (obj?.tag) { - let rval = '('+obj.tag - for(let i=0;;i++) { - let key = 'h'+i - if (!(key in obj)) break - rval += ' ' + go(obj[key]) - } - return rval+')' - } else { - return JSON.stringify(obj) - } - } - return go(obj) + +splitBy : String → Char → List String +splitBy str ch = go Lin Lin (unpack str) + where + go : SnocList String → SnocList Char → List Char → List String + go strs chs Nil = strs <>> (pack (chs <>> Nil) :: Nil) + go strs chs (c :: rest) = + if c == ch then go (strs :< pack (chs <>> Nil)) Lin rest + else go strs (chs :< c) rest + +lines : String → List String +lines str = splitBy str '\n' + + +-- Not as useful as it used to be, we no longer have constructor names +pfunc debugStr : ∀ a. a → String := `(_, obj) => { + return JSON.stringify(obj) }` debugLog : ∀ a. a → IO Unit @@ -508,7 +487,6 @@ pfunc addInt : Int → Int → Int := `(x,y) => x + y` pfunc mulInt : Int → Int → Int := `(x,y) => x * y` pfunc divInt : Int → Int → Int := `(x,y) => x / y | 0` pfunc subInt : Int → Int → Int := `(x,y) => x - y` -pfunc ltInt uses (True False) : Int → Int → Bool := `(x,y) => x < y ? Prelude_True : Prelude_False` instance Mul Int where x * y = mulInt x y @@ -753,8 +731,6 @@ tail (x :: xs) = xs data Ordering = LT | EQ | GT derive Eq Ordering -pfunc jsCompare uses (EQ LT GT) : ∀ a. a → a → Ordering := `(_, a, b) => a == b ? Prelude_EQ : a < b ? Prelude_LT : Prelude_GT` - infixl 6 _<_ _<=_ _>_ class Ord a where compare : a → a → Ordering @@ -776,10 +752,10 @@ instance Ord Nat where compare (S n) (S m) = compare n m instance Ord Int where - compare a b = jsCompare a b + compare a b = if eqInt a b then EQ else if ltInt a b then LT else GT instance Ord Char where - compare a b = jsCompare a b + compare a b = if eqChar a b then EQ else if ltChar a b then LT else GT flip : ∀ a b c. (a → b → c) → (b → a → c) flip f b a = f a b @@ -813,13 +789,13 @@ ite : ∀ a. Bool → a → a → a ite c t e = if c then t else e instance Ord String where - compare a b = jsCompare a b + compare a b = if eqString a b then EQ else if ltString a b then LT else GT instance Cast Int Nat where cast n = intToNat n instance Show Char where - show c = "'\{jsShow c}'" + show c = pack $ '\'' :: c :: '\'' :: Nil swap : ∀ a b. a × b → b × a swap (a,b) = (b,a) @@ -846,8 +822,7 @@ find : ∀ a. (a → Bool) → List a → Maybe a find f Nil = Nothing find f (x :: xs) = if f x then Just x else find f xs --- TODO this would be faster, but less pure as a primitive --- fastConcat might be a good compromise +-- TODO maybe use fastConcat joinBy : String → List String → String joinBy _ Nil = "" joinBy _ (x :: Nil) = x