From f0c9e3bf63e66ec358f951014c5f4bbf8e2733d2 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Thu, 7 Nov 2024 21:05:05 -0800 Subject: [PATCH] Add `Tour.newt` sample and make it the default. Improvements to editor support. --- TODO.md | 4 +- aoc2023/Day1.newt | 5 +- newt-vscode/language-configuration.json | 81 ++++++---- playground/samples/Tour.newt | 197 ++++++++++++++++++++++++ playground/src/main.ts | 31 ++-- playground/src/monarch.ts | 7 + playground/src/worker.ts | 5 +- src/Lib/ProcessDecl.idr | 2 +- 8 files changed, 281 insertions(+), 51 deletions(-) create mode 100644 playground/samples/Tour.newt diff --git a/TODO.md b/TODO.md index 18bf960..f3813a3 100644 --- a/TODO.md +++ b/TODO.md @@ -1,11 +1,13 @@ ## TODO +- [ ] Bad module name error has FC 0,0 instead of the module or name - [x] I've made `{x}` be `{x : _}` instead of `{_ : x}`. Change this. - [ ] Remove context lambdas when printing solutions (show names from context) - build list of names and strip λ, then call pprint with names - [ ] Check for shadowing when declaring dcon - [ ] Require infix decl before declaring names (helps find bugs) +- [ ] sugar for typeclasses - [x] Allow unicode operators/names - Web playground - [x] editor @@ -57,7 +59,7 @@ - [ ] Lean-like .map, etc? (resolve name in namespace of target type, etc) - [x] ~~SKIP list syntax~~ - Agda doesn't have it, clashes with pair syntax -- [ ] autos / typeclass resolution +- [x] autos / typeclass resolution - [x] very primitive version in place, not higher order, search at end - [x] monad is now working - [x] do blocks (needs typeclass, overloaded functions, or constrain to IO) diff --git a/aoc2023/Day1.newt b/aoc2023/Day1.newt index 2f81ce4..a291ddf 100644 --- a/aoc2023/Day1.newt +++ b/aoc2023/Day1.newt @@ -11,9 +11,6 @@ digits1 (c :: cs) = let x = ord c in False => digits1 cs False => digits1 cs --- This happens with Char and not Nat, but why is Char working at all? --- I suspect it will fix if PatLit is implemented correctly - tail : {a : U} -> List a -> List a tail Nil = Nil tail (x :: xs) = xs @@ -51,8 +48,8 @@ part1 text digits = let nums = map combine $ map digits lines in foldl _+_ 0 nums +-- Hack from before I had support for typeclasses infixl 1 _>>_ - _>>_ : {A B : U} -> A -> B -> B a >> b = b diff --git a/newt-vscode/language-configuration.json b/newt-vscode/language-configuration.json index c7fccff..63b9b08 100644 --- a/newt-vscode/language-configuration.json +++ b/newt-vscode/language-configuration.json @@ -1,38 +1,51 @@ { - "comments": { - // symbol used for single line comment. Remove this entry if your language does not support line comments - "lineComment": "--", - // symbols used for start and end a block comment. Remove this entry if your language does not support block comments - "blockComment": [ "/-", "-/" ] + "comments": { + // symbol used for single line comment. Remove this entry if your language does not support line comments + "lineComment": "--", + // symbols used for start and end a block comment. Remove this entry if your language does not support block comments + "blockComment": ["/-", "-/"] + }, + // symbols used as brackets + "brackets": [ + ["{", "}"], + ["{{", "}}"], + ["[", "]"], + ["(", ")"] + ], + // symbols that are auto closed when typing + "autoClosingPairs": [ + ["{", "}"], + ["[", "]"], + ["(", ")"], + ["\"", "\""], + ["'", "'"], + ["/-", "-/"] + ], + // symbols that can be used to surround a selection + "surroundingPairs": [ + ["{", "}"], + ["[", "]"], + ["(", ")"], + ["\"", "\""], + ["'", "'"] + ], + "onEnterRules": [ + { + "beforeText": "\\b(where|of)$", + "action": { "indent": "indent" } }, - // symbols used as brackets - "brackets": [ - ["{", "}"], - ["[", "]"], - ["(", ")"] - ], - // symbols that are auto closed when typing - "autoClosingPairs": [ - ["{", "}"], - ["[", "]"], - ["(", ")"], - ["\"", "\""], - ["'", "'"] - ], - // symbols that can be used to surround a selection - "surroundingPairs": [ - ["{", "}"], - ["[", "]"], - ["(", ")"], - ["\"", "\""], - ["'", "'"] - ], - "onEnterRules": [ - { - "beforeText": "^\\s+$", - "action": { - "indent": "outdent" - } + { + "beforeText": "/-", + "afterText": "-/", + "action": { + "indent": "indentOutdent" } - ] + }, + { + "beforeText": "^\\s+$", + "action": { + "indent": "outdent" + } + } + ] } diff --git a/playground/samples/Tour.newt b/playground/samples/Tour.newt new file mode 100644 index 0000000..0fbe028 --- /dev/null +++ b/playground/samples/Tour.newt @@ -0,0 +1,197 @@ + + +/- + Ok, so this is newt, a dependent typed programming language that + I am implementing to learn how they work. It targets javascript + and borrows a lot of syntax from Idris and Agda. + + This page is a very simple web playground based on the monaco editor. + It runs newt, compiled by Idris2, in a web worker. + + Block comments follow Lean because they're easier to type on a + US keyboard. + + The output, to the right, is somewhat noisy and obtuse. You'll see + INFO and sometimes ERROR messages that show up in the editor view + on hover. I'm emitting INFO for solved metas. + + The Day1.newt and Day2.newt are last year's advent of code, translated + from Lean. You need to visit `Lib.newt` to get it to the worker. + +-/ + +-- One-line comments begin with two hypens + +-- every file begins with a `module` declaration +-- it must match the filename +module Tour + +-- We can import other modules, with a flat namespace and no cycles, +-- diamonds are ok + +-- commented out until we preload other files into the worker +-- import Lib + +-- We're calling the universe U and are doing type in type for now + +-- Inductive type definitions are similar to Idris, Agda, or Haskell +data Nat : U where + Z : Nat + S : Nat -> Nat + +-- Multiple names are allowed on the left: +data Bool : U where + True False : Bool + +-- function definitions are equations using dependent pattern matching +plus : Nat -> Nat -> Nat +plus Z m = m +plus (S n) m = S (plus n m) + +-- we can also have case statements on the right side +-- the core language includes case statements +-- here `\` is used for a lambda expression: +plus' : Nat -> Nat -> Nat +plus' = \ n m => case n of + Z => m + S n => S (plus n m) + +-- We can define operators, currently only infix +-- and we allow unicode and letters in operators +infixl 2 _≡_ + +-- Here is an equality, like Idris, everything goes to the right of the colon +-- Implicits are denoted with braces `{ }` +-- unlike idris, you have to declare all of your implicits +data _≡_ : {A : U} -> A -> A -> U where + Refl : {A : U} {a : A} -> a ≡ a + +-- And now the compiler can verify that 1 + 1 = 2 +test : plus (S Z) (S Z) ≡ S (S Z) +test = Refl + +-- Ok now we do typeclasses. There isn't any sugar, but we have +-- search for implicits marked with double brackets. + +-- Let's say we want a generic `_+_` operator +infixl 7 _+_ + +-- We don't have records yet, so we define a single constructor +-- inductive type: +data Plus : U -> U where + MkPlus : {A : U} -> (A -> A -> A) -> Plus A + +-- and the generic function that uses it +-- the double brackets indicate an argument that is solved by search +_+_ : {A : U} {{_ : Plus A}} -> A -> A -> A +_+_ {{MkPlus f}} x y = f x y + +-- The typeclass is now defined, search will look for functions in scope +-- that return a type matching (same type constructor) the implicit +-- and only have implicit arguments (inspired by Agda). + +-- We make an instance `Plus Nat` +PlusNat : Plus Nat +PlusNat = MkPlus plus + +-- and it now finds the implicits, you'll see the solutions to the +-- implicits if you hover over the `+`. +two : Nat +two = S Z + S Z + +-- We can leave a hole in an expression with ? and the editor will show us the +-- scope and expected type (hover to see) +foo : Nat -> Nat -> Nat +foo a b = ? + +-- Newt compiles to javascript, there is a tab to the right that shows the +-- javascript output. It is not doing erasure (or inlining) yet, so the +-- code is a little verbose. + +-- We can define native types: + +ptype Int : U +ptype String : U +ptype Char : U + +-- The names of these three types are special, primitive numbers, strings, +-- and characters inhabit them, respectively. We can match on primitives, but +-- must provide a default case: + +isVowel : Char -> Bool +isVowel 'a' = True +isVowel 'e' = True +isVowel 'i' = True +isVowel 'o' = True +isVowel 'u' = True +isVowel _ = False + +-- And primitive functions have a type and a javascript definition: + +pfunc plusInt : Int -> Int -> Int := "(x,y) => x + y" +pfunc plusString : String -> String -> String := "(x,y) => x + y" + +-- We can make them Plus instances: + +PlusInt : Plus Int +PlusInt = MkPlus plusInt + +PlusString : Plus String +PlusString = MkPlus plusString + +concat : String -> String -> String +concat a b = a + b + +-- Now we define Monad + +data Monad : (U -> U) -> U where + MkMonad : {m : U -> U} -> + ({a : U} -> a -> m a) -> + ({a b : U} -> m a -> (a -> m b) -> m b) -> + Monad m + +pure : {m : U -> U} -> {{_ : Monad m}} -> {a : U} -> a -> m a +pure {{MkMonad p _}} a = p a + +-- we can declare multiple infix operators at once +infixl 1 _>>=_ _>>_ + +_>>=_ : {m : U -> U} -> {{_ : Monad m}} -> {a b : U} -> m a -> (a -> m b) -> m b +_>>=_ {{MkMonad _ b}} ma amb = b ma amb + +_>>_ : {m : U -> U} -> {{_ : Monad m}} -> {a b : U} -> m a -> m b -> m b +ma >> mb = ma >>= (λ _ => mb) + +-- That's our Monad typeclass, now let's make a List monad + +infixr 3 _::_ +data List : U -> U where + Nil : {A : U} -> List A + _::_ : {A : U} -> A -> List A -> List A + +infixr 7 _++_ +_++_ : {a : U} -> List a -> List a -> List a +Nil ++ ys = ys +(x :: xs) ++ ys = x :: (xs ++ ys) + +bindList : {a b : U} -> List a -> (a -> List b) -> List b +bindList Nil f = Nil +bindList (x :: xs) f = f x ++ bindList xs f + +-- Both `\` and `λ` work for lambda expressions: +MonadList : Monad List +MonadList = MkMonad (λ a => a :: Nil) bindList + +-- We'll want Pair below too. `,` has been left for use as an operator. +-- Also we see that → can be used in lieu of -> +infixr 1 _,_ _×_ +data _×_ : U → U → U where + _,_ : {A B : U} → A → B → A × B + +-- The _>>=_ operator is used for desugaring do blocks + +prod : {A B : U} → List A → List B → List (A × B) +prod xs ys = do + x <- xs + y <- ys + pure (x, y) diff --git a/playground/src/main.ts b/playground/src/main.ts index 4319ec8..a7d9ccb 100644 --- a/playground/src/main.ts +++ b/playground/src/main.ts @@ -33,12 +33,24 @@ const state = { editor: signal(null), }; +async function loadFile(fn: string) { + if (fn) { + const res = await fetch(fn); + const text = await res.text(); + state.editor.value!.setValue(text); + } else { + state.editor.value!.setValue("module Main\n"); + } +} + // I keep pressing this. document.addEventListener("keydown", (ev) => { if (ev.metaKey && ev.code == "KeyS") ev.preventDefault(); }); -let value = localStorage.code || "module Main\n"; +const LOADING = "module Loading\n" + +let value = localStorage.code || LOADING; // let result = document.getElementById("result")!; @@ -62,6 +74,7 @@ function Editor({ initialValue }: EditorProps) { language: "newt", theme: "vs", automaticLayout: true, + unicodeHighlight: { ambiguousCharacters: false }, minimap: { enabled: false }, }); state.editor.value = editor; @@ -74,7 +87,10 @@ function Editor({ initialValue }: EditorProps) { localStorage.code = value; }, 1000); }); - run(initialValue); + if (initialValue === LOADING) + loadFile("Tour.newt") + else + run(initialValue); }, []); return h("div", { id: "editor", ref }); @@ -125,13 +141,13 @@ function Tabs() { } const SAMPLES = [ + "Tour.newt", "Tree.newt", // "Prelude.newt", "Lib.newt", "Day1.newt", "Day2.newt", "TypeClass.newt", - ]; function EditWrap() { @@ -141,13 +157,8 @@ function EditWrap() { if (ev.target instanceof HTMLSelectElement) { let fn = ev.target.value; ev.target.value = ""; - if (fn) { - const res = await fetch(fn); - const text = await res.text(); - state.editor.value!.setValue(text); - } else { - state.editor.value!.setValue("module Main\n"); - } + loadFile(fn) + } }; return h( diff --git a/playground/src/monarch.ts b/playground/src/monarch.ts index cebb5c3..b0657b0 100644 --- a/playground/src/monarch.ts +++ b/playground/src/monarch.ts @@ -48,6 +48,13 @@ export let newtConfig: monaco.languages.LanguageConfiguration = { indentAction: monaco.languages.IndentAction.Indent, }, }, + { + beforeText: /\/-/, + afterText: /-\//, + action: { + indentAction: monaco.languages.IndentAction.IndentOutdent, + }, + }, ], }; diff --git a/playground/src/worker.ts b/playground/src/worker.ts index 64c3916..1b769f1 100644 --- a/playground/src/worker.ts +++ b/playground/src/worker.ts @@ -130,6 +130,7 @@ onmessage = function (e) { files[fn] = src; files['out.js'] = 'No JS output'; stdout = '' + const start = +new Date() try { newtMain(); } catch (e) { @@ -138,7 +139,9 @@ onmessage = function (e) { // make it visable stdout += '\n' + String(e) } + let duration = +new Date() - start + console.log(`process ${fn} in ${duration} ms`) let javascript = files['out.js'] let output = stdout - postMessage({javascript, output}) + postMessage({javascript, output, duration}) } diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 5e3aa92..7dd8a4a 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -132,7 +132,7 @@ logMetas mstart = do let names = (toList $ map fst ctx.types) -- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too. env <- for (zip ctx.env (toList ctx.types)) $ \(v, n, ty) => pure " \{n} : \{pprint names !(quote ctx.lvl ty)} = \{pprint names !(quote ctx.lvl v)}" - let msg = "\{unlines (toList $ reverse env)} -----------\n \{pprint names ty'}\n \{showTm ty'}" + let msg = "\{unlines (toList $ reverse env)} -----------\n \{pprint names ty'}" info fc "User Hole\n\{msg}" (Unsolved (l,c) k ctx ty kind cons) => do tm <- quote ctx.lvl !(forceMeta ty)