Search includes scope, tweak to code formatting

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

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

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