Add Tour.newt sample and make it the default.

Improvements to editor support.

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)

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
 

newt-vscode/language-configuration.json

@@ -8,6 +8,7 @@
   // symbols used as brackets
   "brackets": [
     ["{", "}"],
+    ["{{", "}}"],
     ["[", "]"],
     ["(", ")"]
   ],
@@ -17,7 +18,8 @@
     ["[", "]"],
     ["(", ")"],
     ["\"", "\""],
-        ["'", "'"]
+    ["'", "'"],
+    ["/-", "-/"]
   ],
   // symbols that can be used to surround a selection
   "surroundingPairs": [
@@ -28,6 +30,17 @@
     ["'", "'"]
   ],
   "onEnterRules": [
+    {
+      "beforeText": "\\b(where|of)$",
+      "action": { "indent": "indent" }
+    },
+    {
+      "beforeText": "/-",
+      "afterText": "-/",
+      "action": {
+        "indent": "indentOutdent"
+      }
+    },
     {
       "beforeText": "^\\s+$",
       "action": {

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)

playground/src/main.ts

@@ -33,12 +33,24 @@ const state = {
   editor: signal<monaco.editor.IStandaloneCodeEditor | null>(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,6 +87,9 @@ function Editor({ initialValue }: EditorProps) {
         localStorage.code = value;
       }, 1000);
     });
+    if (initialValue === LOADING)
+      loadFile("Tour.newt")
+    else
       run(initialValue);
   }, []);
 
@@ -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) {
+      loadFile(fn)
-        const res = await fetch(fn);
+
-        const text = await res.text();
-        state.editor.value!.setValue(text);
-      } else {
-        state.editor.value!.setValue("module Main\n");
-      }
     }
   };
   return h(

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,
+      },
+    },
   ],
 };
 

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})
 }

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)