Cleanup and a fix to Prelude and the playground

README.md

@@ -6,13 +6,13 @@ my first attempt to write a dependent typed language. It is inspired by Idris,
 Elaboration Zoo, pi-forall, and other tutorials.
 
 It has inductive types, dependent pattern matching, a typeclass-like mechanism, compiles
-to javascript, and is self hosted. There is a browser playground and vscode extension.
+to javascript, and is now written in itself. There is a browser playground and vscode extension.
 
 The web playground can be at https://dunhamsteve.github.io/newt. The top left corner
 has a dropdown with some samples. Currently the web playground is using the Idris-built
 version of newt because most browsers lack tail call optimization.
 
-The directory `port` contains a port of newt to itself. Currently it needs to be run by `bun` rather than `node` because `newt` does not do any transformations for TCO and JavaScriptCore is the only javascript implementation that does TCO.
+The directory `port` contains a port of newt to itself. Currently it needs to be run by `bun` rather than `node` because `bun` does tail call optimization.
 
 ## Sample code
 
@@ -46,29 +46,30 @@ doing `subst`.
 
 The raw syntax is `Raw`. This is elaborated to `Tm`. There is a top level context and a
 context during checking. The top level context uses names, and type checking uses deBruijn
-indices for `Tm` and levels for `Val`.  For compilation, this is converted to `CExp`, which works out how arity and closures will work, and then `JSExp` which is javascript AST.
+indices for `Tm` and levels for `Val`.  For compilation, this is converted to `CExp`, which works out how arity and closures will work, and then into `JSExp` which is javascript AST.
 
-I have `Let` in the core language. Partly because I'd like this to make it into javascript (only compute once), but also because it's being leveraged by the casetree stuff.
+I have `Let` in the core language. Partly because I'd like this to make it into javascript (only compute once), but also because it's being leveraged by the casetree stuff. The `where` clauses are turned into `LetRec` and locally defined functions, so I'm punting the lambda-lifting to javascript for now.
 
-I also have `Case` in the core language.
+`Case` is in the core language `Tm` and it can appear anywhere in the syntax tree.
 
 ## Case Tree
 
-I've got no idea what I'm doing here. I worked off of Jesper Cockx "Elaborating Dependent (Co)pattern Matching", leaving out codata for now.  I've now added matching primitives, requiring a default case. When splitting on inductive types it will break out all of the remaining cases and doesn't emit a default case.
+This is inspired by Jesper Cockx "Elaborating Dependent (Co)pattern Matching". I've left off codata for now, and I'm trying to do indexes on the types rather than having explicit equalities as arguments. I've also added matching on primitives, which require a default case. And when matching on inductive types, I collect the unmentioned, but relevant constructors into a single default case. This greatly improved performance and reduced the size of the emitted code.
+
 
 I'm essentially putting the constraints into the environment like `let`. This is a problem when stuff is already in `Val` form. Substitution into types in the context is done via quote/eval. I plan to revisit this.
 
-I intend to add the codata / copatterns from the paper, but haven't gotten to that yet.
-
 ## Evaluation
 
 Following kovacs, I'm putting `VVar` into context env when I go under binders in type-checking. This avoids substitution.
 
 ## Autos
 
-Newt has primitive auto implicits. They are denoted by double braces `{{}}` as in Agda. Newt will search for a function that returns a type in the same family, only has implicit and auto-implicit arguments, and unifies (satisfying any relevant constraints).
+Auto implicits are denoted by double braces `{{}}`.  They are solved by searching for functions that return a type heading by the same type constructor and have only implicit and auto implicit arguments. It tries to solve the implicit with each candidate by checking it against the type, allowing one level of constraint to be checked. If exactly one works, it will take that as a solution and proceed.
 
-This search can be used to manually create typeclasses.  `do` blocks are supported, desugaring to `>>=`, which it expects to be the `bind` of a Monad typeclass.
+Otherwise, we rarely solve the type because it contains metas with constraints that don't work with pattern unification (they have extra arguments).  I stop at one constraint to try to handle cases where a type mismatch gets turned into an auto failing to be solved.
+
+The sugar for `do` blocks uses the `>>=` operator, which is defined on the `Monad` interface in the `Prelude`.
 
 ## References
 

newt/Prelude.newt

@@ -472,7 +472,7 @@ foldr f b Nil = b
 foldr f b (x :: xs) = f x (foldr f b xs)
 
 infixl 9 _∘_
-_∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
+_∘_ : ∀ A B C. (B -> C) -> (A -> B) -> A -> C
 (f ∘ g) x = f (g x)
 
 

playground/src/main.ts

@@ -227,8 +227,9 @@ const ABBREV: Record<string, string> = {
     '\\all': '∀',
     '\\\\': '\\',
     '\\==': '≡',
-    '\circ': '∘',
+    '\\circ': '∘',
-    '\\_1': '₁',
+    '\\1': '₁',
+    '\\2': '₂',
   }
 
 function Editor({ initialValue }: EditorProps) {

port/Lib/Elab.newt

@@ -15,15 +15,12 @@ import Lib.TopContext
 import Lib.Syntax
 import Lib.Types
 
-
 vprint : Context -> Val -> M String
 vprint ctx v = do
   tm <- quote (length' ctx.env) v
   pure $ render 90 $ pprint (names ctx) tm
 
-
 -- collectDecl collects multiple Def for one function into one
-
 collectDecl : List Decl -> List Decl
 collectDecl Nil = Nil
 collectDecl ((Def fc nm cl) :: rest@(Def _ nm' cl' :: xs)) =
@@ -34,10 +31,6 @@ collectDecl (x :: xs) = x :: collectDecl xs
 rpprint : List String → Tm → String
 rpprint names tm = render 90 $ pprint names tm
 
--- renaming
--- dom gamma ren
-data Pden = PR Int Int (List Int)
-
 showCtx : Context -> M String
 showCtx ctx =
   unlines ∘ reverse <$> go (names ctx) 0 (reverse $ zip ctx.env ctx.types) Nil
@@ -70,10 +63,7 @@ dumpCtx ctx = do
   let msg = unlines (reverse env) -- ++ "  -----------\n" ++ "  goal \{rpprint names ty'}"
   pure msg
 
-
-
 -- return Bnd and type for name
-
 lookupName : Context -> String  -> Maybe (Tm × Val)
 lookupName ctx name = go 0 ctx.types
   where
@@ -82,7 +72,6 @@ lookupName ctx name = go 0 ctx.types
     -- FIXME - we should stuff a Binder of some sort into "types"
     go ix ((nm, ty) :: xs) = if nm == name then Just (Bnd emptyFC ix, ty) else go (1 + ix) xs
 
-
 lookupDef : Context -> String  -> Maybe Val
 lookupDef ctx name = go 0 ctx.types ctx.env
   where
@@ -90,9 +79,6 @@ lookupDef ctx name = go 0 ctx.types ctx.env
     go ix ((nm, ty) :: xs) (v :: vs) = if nm == name then Just v else go (1 + ix) xs vs
     go ix _ _ = Nothing
 
-
--- IORef for metas needs IO
-
 forceMeta : Val -> M Val
 forceMeta (VMeta fc ix sp) = do
   meta <- lookupMeta ix
@@ -101,7 +87,6 @@ forceMeta (VMeta fc ix sp) = do
     _ => pure (VMeta fc ix sp)
 forceMeta x = pure x
 
-
 record UnifyResult where
   constructor MkResult
   -- wild guess here - lhs is a VVar
@@ -115,11 +100,8 @@ instance Monoid UnifyResult where
 
 data UnifyMode = UNormal | UPattern
 
-
-
 check : Context -> Raw -> Val -> M Tm
 
-
 unifyCatch : FC -> Context -> Val -> Val -> M Unit
 
 -- Check that the arguments are not explicit and the type constructor in codomain matches
@@ -132,26 +114,18 @@ isCandidate (VRef _ nm _) (Ref fc nm') = nm == nm'
 isCandidate ty (App fc t u) = isCandidate ty t
 isCandidate _ _ = False
 
--- This is a crude first pass
-
 findMatches : Context -> Val -> List TopEntry -> M (List String)
 findMatches ctx ty Nil = pure Nil
 findMatches ctx ty ((MkEntry _ name type def) :: xs) = do
   let (True) = isCandidate ty type | False => findMatches ctx ty xs
   top <- get
-  -- let ctx = mkCtx (getFC ty)
-  -- FIXME we're restoring state, but the INFO logs have already been emitted
-  -- Also redo this whole thing to run during elab, recheck constraints, etc.
   mc <- readIORef top.metaCtx
   catchError (do
       -- TODO sort out the FC here
       let fc = getFC ty
       debug $ \ _ => "TRY \{show name} : \{rpprint Nil type} for \{show ty}"
       -- This check is solving metas, so we save mc below in case we want this solution
-      -- tm <- check (mkCtx fc) (RVar fc name) ty
-      -- FIXME RVar should optionally have qualified names
       let (QN ns nm) = name
-
       let (cod, tele) = splitTele type
       modifyIORef top.metaCtx $ \ mc => MC mc.metas mc.next CheckFirst
       tm <- check ctx (RVar fc nm) ty
@@ -163,7 +137,6 @@ findMatches ctx ty ((MkEntry _ name type def) :: xs) = do
       writeIORef top.metaCtx mc
       findMatches ctx ty xs)
 
-
 contextMatches : Context -> Val -> M (List (Tm × Val))
 contextMatches ctx ty = go (zip ctx.env ctx.types)
   where
@@ -186,28 +159,19 @@ contextMatches ctx ty = go (zip ctx.env ctx.types)
           writeIORef top.metaCtx mc
           go xs)
 
-
 getArity : Tm -> Int
 getArity (Pi x str icit rig t u) = 1 + getArity u
 -- Ref or App (of type constructor) are valid
 getArity _ = 0
 
--- Can metas live in context for now?
--- We'll have to be able to add them, which might put gamma in a ref
-
-
-
 -- Makes the arg for `solve` when we solve an auto
 makeSpine : Int -> List BD -> SnocList Val
 makeSpine k Nil = Lin
 makeSpine k (Defined :: xs) = makeSpine (k - 1) xs
 makeSpine k (Bound :: xs) = makeSpine (k - 1) xs :< VVar emptyFC (k - 1) Lin
 
-
 solve : Env -> QName -> SnocList Val -> Val -> M Unit
 
-
-
 trySolveAuto : MetaEntry -> M Bool
 trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do
       debug $ \ _ => "TRYAUTO solving \{show k} : \{show ty}"
@@ -244,33 +208,12 @@ trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do
       pure True
 trySolveAuto _ = pure False
 
--- export
+solveAutos : M Unit
--- solveAutos : Int -> List MetaEntry -> M Unit
+solveAutos = do
--- solveAutos mstart Nil = pure MkUnit
--- solveAutos mstart (entry :: es) = do
---       res <- trySolveAuto entry
---       -- idris is inlining this and blowing stack?
---       if res
---         then do
---           top <- get
---           mc <- readIORef top.metaCtx
---           let mlen = length mc.metas `minus` mstart
---           solveAutos mstart (take mlen mc.metas)
---         else
---           solveAutos mstart es
-
-
--- Called from ProcessDecl, this was popping the stack, the tail call optimization doesn't
--- handle the traversal of the entire meta list.  I've turned the restart into a trampoline
--- and filtered it down to unsolved autos.
-
-solveAutos : Int -> M Unit
-solveAutos mstart = do
   top <- get
   mc <- readIORef top.metaCtx
-
   res <- run $ filter isAuto (listValues mc.metas)
-  if res then solveAutos mstart else pure MkUnit
+  if res then solveAutos else pure MkUnit
   where
     isAuto : MetaEntry -> Bool
     isAuto (Unsolved fc k ctx x AutoSolve xs) = True
@@ -292,7 +235,6 @@ updateMeta ix f = do
   me <- f me
   writeIORef top.metaCtx $ MC (updateMap ix me mc.metas) mc.next mc.mcmode
 
-
 checkAutos : QName -> List MetaEntry -> M Unit
 checkAutos ix Nil = pure MkUnit
 checkAutos ix (entry@(Unsolved fc k ctx ty AutoSolve _) :: rest) = do
@@ -306,7 +248,6 @@ checkAutos ix (entry@(Unsolved fc k ctx ty AutoSolve _) :: rest) = do
     usesMeta _ = False
 checkAutos ix (_ :: rest) = checkAutos ix rest
 
-
 addConstraint : Env -> QName -> SnocList Val -> Val -> M Unit
 addConstraint env ix sp tm = do
   top <- get
@@ -320,11 +261,8 @@ addConstraint env ix sp tm = do
     (OutOfScope) => error' "Meta \{show ix} out of scope"
   mc <- readIORef top.metaCtx
   checkAutos ix (listValues mc.metas)
-  -- this loops too
-  -- solveAutos 0 mc.metas
   pure MkUnit
 
-
 -- return renaming, the position is the new VVar
 invert : Int -> SnocList Val -> M (List Int)
 invert lvl sp = go sp Nil
@@ -340,12 +278,6 @@ invert lvl sp = go sp Nil
         else go xs (k :: acc)
     go (xs :< v) _ = error emptyFC "non-variable in pattern \{show v}"
 
-
--- REVIEW why am I converting to Tm?
--- we have to "lift" the renaming when we go under a lambda
--- I think that essentially means our domain ix are one bigger, since we're looking at lvl
--- in the codomain, so maybe we can just keep that value
-
 rename : QName -> List Int -> Int -> Val  -> M Tm
 
 renameSpine : QName -> List Int -> Int -> Tm -> SnocList Val  -> M Tm
@@ -406,7 +338,6 @@ lams Z _ tm = tm
 lams (S k) Nil tm = Lam emptyFC "arg_\{show k}" Explicit Many (lams k Nil tm)
 lams (S k) (x :: xs) tm = Lam emptyFC x Explicit Many (lams k xs tm)
 
-
 unify : Env -> UnifyMode -> Val -> Val  -> M UnifyResult
 
 .boundNames : Context -> List String
@@ -485,7 +416,6 @@ unifySpine env mode True (xs :< x) (ys :< y) =
   _<+>_ <$> unify env mode x y <*> unifySpine env mode True xs ys
 unifySpine env mode True _ _ = error emptyFC "meta spine length mismatch"
 
-
 unify env mode t u = do
   debug $ \ _ => "Unify lvl \{show $ length env}"
   debug $ \ _ => "  \{show t}"
@@ -623,7 +553,6 @@ unify env mode t u = do
     unifyPattern t (VVar fc k Lin) = pure $ MkResult ((k, t) :: Nil)
     unifyPattern t u = unifyMeta t u
 
-
 unifyCatch fc ctx ty' ty = do
     res <- catchError (unify ctx.env UNormal ty' ty) $ \err => do
       let names = map fst ctx.types
@@ -646,7 +575,6 @@ unifyCatch fc ctx ty' ty = do
         throwError (E fc msg)
         -- error fc "Unification yields constraints \{show cs.constraints}"
 
-
 freshMeta : Context -> FC -> Val -> MetaKind -> M Tm
 freshMeta ctx fc ty kind = do
   top <- get
@@ -695,19 +623,15 @@ primType fc nm = do
       Just (MkEntry _ name ty PrimTCon) => pure $ VRef fc name Lin
       _ => error fc "Primitive type \{show nm} not in scope"
 
-
 infer : Context -> Raw  -> M (Tm × Val)
 
-
 data Bind = MkBind String Icit Val
 
 instance Show Bind where
   show (MkBind str icit x) = "\{str} \{show icit}"
 
-
 ---------------- Case builder
 
-
 record Problem where
   constructor MkProb
   clauses : List Clause
@@ -747,7 +671,6 @@ findSplit (x@(nm, PatCon _ _ _ _ _) :: xs) = Just x
 findSplit (x@(nm, PatLit _ val) :: xs) = Just x
 findSplit (x :: xs) = findSplit xs
 
-
 -- ***************
 -- right, I think we rewrite the names in the context before running raw and we're good to go?
 -- We have stuff like S k /? x, but I think we can back up to whatever the scrutinee variable was?
@@ -811,7 +734,6 @@ substVal k v tm = go tm
     -- go (VU x) = ?rhs_7
     -- go (VLit x y) = ?rhs_8
 
-
 -- need to turn k into a ground value
 
 -- TODO rework this to do something better.  We've got constraints, and
@@ -1037,15 +959,12 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
       Just cons <- rewriteConstraint sctynm vars cons Nil | _ => pure Nothing
       pure $ Just $ MkClause fc cons pats expr
 
-
 splitArgs : Raw -> List (Raw × Icit) -> (Raw × List (Raw × Icit))
 splitArgs (RApp fc t u icit) args = splitArgs t ((u, icit) :: args)
 splitArgs tm args = (tm, args)
 
-
 mkPat : (Raw × Icit) -> M Pattern
 mkPat (RAs fc as tm, icit) = do
-
   pat <- mkPat (tm, icit)
   case pat of
     (PatCon fc icit nm args Nothing) => pure $ PatCon fc icit nm args (Just as)
@@ -1070,16 +989,12 @@ mkPat (tm, icit) = do
     ((RLit fc y), b) => error fc "lit cannot be applied to arguments"
     (a,b) => error (getFC a) "expected pat var or constructor, got \{show a}"
 
-
-
 makeClause : (Raw × Raw) -> M Clause
 makeClause (lhs, rhs) = do
   let (nm, args) = splitArgs lhs Nil
   pats <- traverse mkPat args
   pure $ MkClause (getFC lhs) Nil pats rhs
 
-
-
 -- we'll want both check and infer, we're augmenting a context
 -- so probably a continuation:
 -- Context -> List Decl -> (Context -> M a) -> M a
@@ -1310,7 +1225,7 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints Nil expr) :: cs) ty) = do
           top <- get
           mc <- readIORef top.metaCtx
           -- TODO - only hit the relevant ones
-          ignore $ solveAutos 0
+          solveAutos
           forceType ctx.env scty'
         OutOfScope => pure scty'
 
@@ -1364,7 +1279,6 @@ showDef ctx names n v@(VVar _ n' Lin) =  if n == n'
 showDef ctx names n v = do
   vv <- vprint ctx v
   pure "= \{vv}"
-  -- pure "= \{rpprint names !(quote ctx.lvl v)}"
 
 -- desugar do
 undo : FC -> List DoStmt -> M Raw
@@ -1446,7 +1360,6 @@ check ctx tm ty = do
               pty <- prvalCtx ty
               error fc "Expected pi type, got \{pty}"
 
-
     (RLet fc nm ty v sc, rty) => do
       ty' <- check ctx ty (VU emptyFC)
       vty <- eval ctx.env CBN ty'

port/Lib/ProcessDecl.newt

@@ -154,7 +154,7 @@ processDecl ns (Def fc nm clauses) = do
   -- putStrLn "Ok \{render 90 $ pprint Nil tm}"
 
   mc <- readIORef top.metaCtx
-  solveAutos 0
+  solveAutos
   -- TODO - make nf that expands all metas and drop zonk
   -- Idris2 doesn't expand metas for performance - a lot of these are dropped during erasure.
   -- Day1.newt is a test case

src/Lib/Eval.idr

@@ -25,7 +25,6 @@ public export
 ($$) : {auto mode : Mode} -> Closure -> Val -> M Val
 ($$) {mode} (MkClosure env tm) u = eval (u :: env) mode tm
 
-
 export
 vapp : Val -> Val -> M Val
 vapp (VLam _ _ _ _ t) u = t $$ u
@@ -41,8 +40,6 @@ vappSpine t (xs :< x) = do
   rest <- vappSpine t xs
   vapp rest x
 
-
-
 lookupVar : Env -> Nat -> Maybe Val
 lookupVar env k = let l = length env in
   if k > l
@@ -85,7 +82,6 @@ tryEval env (VRef fc k _ sp) = do
       _ => pure Nothing
 tryEval _ _ = pure Nothing
 
-
 -- Force far enough to compare types
 export
 forceType : Env -> Val -> M Val
@@ -138,13 +134,6 @@ evalCase env mode sc cc = do
   debug "env is \{show env}"
   pure Nothing
 
--- So smalltt says:
---   Smalltt has the following approach:
---   - Top-level and local definitions are lazy.
---   - We instantiate Pi types during elaboration with lazy values.
---   - Applications headed by top-level variables are lazy.
---   - Any other function application is call-by-value during evaluation.
-
 -- TODO maybe add glueing
 
 eval env mode (Ref fc x def) = pure $ VRef fc x def [<]
@@ -192,7 +181,6 @@ eval env mode tm@(Case fc sc alts) = do
 export
 quote : (lvl : Nat) -> Val -> M Tm
 
-
 quoteSp : (lvl : Nat) -> Tm -> SnocList Val -> M Tm
 quoteSp lvl t [<] = pure t
 quoteSp lvl t (xs :< x) = do
@@ -250,20 +238,6 @@ prvalCtx v = do
   tm <- quote ctx.lvl v
   pure $ interpolate $ pprint (toList $ map fst ctx.types) tm
 
--- REVIEW - might be easier if we inserted the meta without a bunch of explicit App
--- I believe Kovacs is doing that.
-
--- we need to walk the whole thing
--- meta in Tm have a bunch of args, which should be the relevant
--- parts of the scope. So, meta has a bunch of lambdas, we've got a bunch of
--- args and we need to beta reduce, which seems like a lot of work for nothing
--- Could we put the "good bits" of the Meta in there and write it to Bnd directly
--- off of scope? I guess this might get dicey when a meta is another meta applied
--- to something.
-
--- ok, so we're doing something that looks lot like eval, having to collect args,
--- pull the def, and apply spine. Eval is trying for WHNF, so it doesn't walk the
--- whole thing. (We'd like to insert metas inside lambdas.)
 export
 zonk : TopContext -> Nat -> Env -> Tm -> M Tm