From 375c16f4fdf0ac0d073c84f42beba54a2c22ba57 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Wed, 6 Nov 2024 20:53:44 -0800
Subject: [PATCH] Search includes scope, tweak to code formatting

---
 TODO.md                    | 16 ++++++++-----
 src/Lib/Compile.idr        |  4 ++--
 src/Lib/Elab.idr           |  2 +-
 src/Lib/ProcessDecl.idr    | 46 +++++++++++++++++++++++++++++---------
 tests/black/TestCase5.newt | 35 +++++++++++++++++++++++++++++
 5 files changed, 84 insertions(+), 19 deletions(-)
 create mode 100644 tests/black/TestCase5.newt

diff --git a/TODO.md b/TODO.md
index ba01984..7190b72 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,15 +1,21 @@
 
 ## TODO
 
+- [ ] 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
+- [ ] Require infix decl before declaring names (helps find bugs)
 - [x] Allow unicode operators/names
-- [ ] Web tool
-  - edit, view output, view js, run js, monaco would be nice.
-  - need to shim out Buffer
+- Web playground
+  - [x] editor
+  - [x] view output
+  - [x] view javascript
+  - [ ] run javascript
+  - [x] need to shim out Buffer
 - [x] get rid of stray INFO from auto resolution
 - [ ] handle `if_then_else_` style mixfix
-- [ ] Search should look at context
+- [x] Search should look at context
 - [ ] records
 - [ ] copattern matching
 - [ ] Support @ on the LHS
diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr
index fea793f..c1ad233 100644
--- a/src/Lib/Compile.idr
+++ b/src/Lib/Compile.idr
@@ -191,7 +191,7 @@ stmtToDoc : JSStmt e -> Doc
 ||| separate with space
 export
 commaSep : List Doc -> Doc
-commaSep = folddoc (\a, b => a ++ "," <+> b)
+commaSep = folddoc (\a, b => a ++ "," <+/> b)
 
 expToDoc : JSExp -> Doc
 expToDoc (LitArray xs) = ?expToDoc_rhs_0
@@ -203,7 +203,7 @@ expToDoc (LitObject xs) = text "{" <+> folddoc (\ a, e => a ++ ", " <+/> e) (map
 
 expToDoc (LitString str) = jsString str
 expToDoc (LitInt i) = text $ show i
-expToDoc (Apply x xs) = expToDoc x ++ "(" ++ commaSep (map expToDoc xs) ++ ")"
+expToDoc (Apply x xs) = expToDoc x ++ "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ ")"
 expToDoc (Var nm) = jsIdent nm
 expToDoc (JLam nms (JReturn exp)) = text "(" <+> commaSep (map jsIdent nms) <+> ") =>" <+> "(" ++ expToDoc exp ++ ")"
 expToDoc (JLam nms body) = text "(" <+> commaSep (map jsIdent nms) <+> ") =>" <+> bracket "{" (stmtToDoc body) "}"
diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr
index 4c716f7..296e418 100644
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -320,7 +320,7 @@ parameters (ctx: Context)
             Just v => Just v
             Nothing => Nothing
 
-
+export
 unifyCatch : FC -> Context -> Val -> Val -> M ()
 unifyCatch fc ctx ty' ty = do
     res <- catchError (unify ctx ctx.lvl Normal ty' ty) $ \(E x str) => do
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index a066023..5e3aa92 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -22,15 +22,14 @@ isCandidate (VRef _ nm _ _) (Ref fc nm' def) = nm == nm'
 isCandidate ty (App fc t u) = isCandidate ty t
 isCandidate _ _ = False
 
-
 -- This is a crude first pass
 -- TODO consider ctx
-findMatches : Val -> List TopEntry -> M (List (Tm, MetaContext))
-findMatches ty [] = pure []
-findMatches ty ((MkEntry name type def@(Fn t)) :: xs) = do
-  let True = isCandidate ty type | False => findMatches ty xs
+findMatches : Context -> Val -> List TopEntry -> M (List (Tm, MetaContext))
+findMatches ctx ty [] = pure []
+findMatches ctx ty ((MkEntry name type def@(Fn t)) :: xs) = do
+  let True = isCandidate ty type | False => findMatches ctx ty xs
   top <- get
-  let ctx = mkCtx top.metas (getFC ty)
+  -- let ctx = mkCtx top.metas (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.metas
@@ -39,16 +38,39 @@ findMatches ty ((MkEntry name type def@(Fn t)) :: xs) = do
       let fc = getFC ty
       debug "TRY \{name} : \{pprint [] type} for \{show ty}"
       -- This check is solving metas, so we save mc below in case we want this solution
-      tm <- check (mkCtx top.metas fc) (RVar fc name) ty
+      -- tm <- check (mkCtx top.metas fc) (RVar fc name) ty
+      tm <- check ctx (RVar fc name) ty
       debug "Found \{pprint [] tm} for \{show ty}"
       mc' <- readIORef top.metas
       writeIORef top.metas mc
-      ((tm, mc') ::) <$> findMatches ty xs)
+      ((tm, mc') ::) <$> findMatches ctx ty xs)
     (\ err => do
       debug "No match \{show ty} \{pprint [] type} \{showError "" err}"
       writeIORef top.metas mc
-      findMatches ty xs)
-findMatches ty (y :: xs) = findMatches ty xs
+      findMatches ctx ty xs)
+findMatches ctx ty (y :: xs) = findMatches ctx ty xs
+
+contextMatches : Context -> Val -> M (List (Tm, MetaContext))
+contextMatches ctx ty = go (zip ctx.env (toList ctx.types))
+  where
+    go : List (Val, String, Val) -> M (List (Tm, MetaContext))
+    go [] = pure []
+    go ((tm, nm, vty) :: xs) = do
+      type <- quote ctx.lvl vty
+      let True = isCandidate ty type | False => go xs
+      top <- get
+      mc <- readIORef top.metas
+      catchError {e=Error} (do
+          debug "TRY context \{nm} : \{pprint (names ctx) type} for \{show ty}"
+          unifyCatch (getFC ty) ctx ty vty
+          mc' <- readIORef top.metas
+          writeIORef top.metas mc
+          tm <- quote ctx.lvl tm
+          ((tm, mc') ::) <$> go xs)
+        (\ err => do
+          debug "No match \{show ty} \{pprint (names ctx) type} \{showError "" err}"
+          writeIORef top.metas mc
+          go xs)
 
 getArity : Tm -> Nat
 getArity (Pi x str icit t u) = S (getArity u)
@@ -80,7 +102,9 @@ solveAutos mlen ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
       debug "AUTO solving \{show k} : \{show ty}"
       -- we want the context here too.
       top <- get
-      [(tm,mc)] <- findMatches ty top.defs
+      [(tm, mc)] <- case !(contextMatches ctx ty) of
+            [] => findMatches ctx ty top.defs
+            xs => pure xs
         | res => do
           debug "FAILED to solve \{show ty}, matches: \{show $ map (pprint [] . fst) res}"
           solveAutos mlen es
diff --git a/tests/black/TestCase5.newt b/tests/black/TestCase5.newt
new file mode 100644
index 0000000..a700eb9
--- /dev/null
+++ b/tests/black/TestCase5.newt
@@ -0,0 +1,35 @@
+module TestCase5
+
+-- last bit tests pulling solutions from context
+
+data Plus : U -> U where
+    MkPlus : {A : U} -> (A -> A -> A) -> Plus A
+
+infixl 7 _+_
+_+_ : {A : U} {{_ : Plus A}} -> A -> A -> A
+_+_ {{MkPlus plus}} x y = plus x y
+
+ptype Int
+pfunc plusInt : Int -> Int -> Int := "(x,y) => x + y"
+
+PlusInt : Plus Int
+PlusInt = MkPlus plusInt
+
+-- TODO this needs some aggressive inlining...
+double : Int -> Int
+double x = x + x
+
+data Nat : U where
+    Z : Nat
+    S : Nat -> Nat
+
+plus : Nat -> Nat -> Nat
+plus Z m = m
+plus (S n) m = S (plus n m)
+
+PlusNat : Plus Nat
+PlusNat = MkPlus plus
+
+double2 : {A : U} {{foo : Plus A}} -> A -> A
+double2 = \ a => a + a
+