import action for out of scope names, start introducing error types

src/Commands.newt

@@ -26,17 +26,18 @@ decomposeName fn =
             else (joinBy "/" (xs :< x <>> Nil), joinBy "." acc)
 
 
-switchModule : FileSource → String → M ModContext
+switchModule : FileSource → String → M (Maybe ModContext)
 switchModule repo modns = do
-    mod <- processModule emptyFC repo Nil modns
+    top <- getTop
+    let (Just mod) = lookupMap' modns top.modules | Nothing => pure Nothing
     modifyTop [ currentMod := mod; ops := mod.modOps ]
-    pure mod
+    pure $ Just mod
 
 -- The cheap version of type at point, find the token, lookup in global context
 -- Later we will either get good FC for entries or scan them all and build a cache.
 getHoverInfo : FileSource → String → Int → Int → M (Maybe (String × FC))
 getHoverInfo repo modns row col = do
-    mod <- switchModule repo modns
+    Just mod <- switchModule repo modns | _ => pure Nothing
     top <- getTop
 
     -- Find the token at the point
@@ -61,6 +62,8 @@ data FileEdit = MkEdit FC String
 data CodeAction
   = CaseSplitAction (List FileEdit)
   | AddMissingAction (List FileEdit)
+  | Intro String FileEdit
+  | ImportAction String FileEdit
 
 
 applyDCon : QName × Int × Tm → List String
@@ -71,12 +74,15 @@ applyDCon (QN _ nm, _, tm) = go (Lin :< nm) tm
     go acc (Pi _ _ _ _ _ u) = go acc u
     go acc _ = acc <>> Nil
 
+data Flavor = EqSplit | FatArrowSplit | MonadSplit
+
 -- Not quite right, we also need to check for let...
 -- But it's a first pass
-splitEquals : SnocList Char → List Char → (Bool × String × String)
-splitEquals acc Nil = (True, pack (acc <>> Nil), "")
-splitEquals acc xs@('=' :: _) = (True, pack (acc <>> Nil), pack xs)
-splitEquals acc xs@('<' :: '-' :: _) = (False, pack (acc <>> Nil), pack xs)
+splitEquals : SnocList Char → List Char → (Flavor × String × String)
+splitEquals acc Nil = (EqSplit, pack (acc <>> Nil), "")
+splitEquals acc xs@('=' :: '>' :: _) = (FatArrowSplit, pack (acc <>> Nil), pack xs)
+splitEquals acc xs@('=' :: _) = (EqSplit, pack (acc <>> Nil), pack xs)
+splitEquals acc xs@('<' :: '-' :: _) = (MonadSplit, pack (acc <>> Nil), pack xs)
 splitEquals acc (x :: xs) = splitEquals (acc :< x) xs
 
 needParens : SnocList Char → List Char → Bool
@@ -114,20 +120,23 @@ makeEdits fc@(MkFC uri (MkBounds sr sc er ec)) names inPlace = do
   let cs = unpack line
   let head = take (cast sc) cs
   let tail = drop (S $ cast (ec - 1)) cs
-  let (isEq, before, after) = splitEquals Lin tail
+  let (splitKind, before, after) = splitEquals Lin tail
   let np = needParens (Lin <>< head) tail
   let cons = map (addParens np ∘ resugarOper) cons
   let phead = pack head
+  let indent = getIndent 0 head
+  let nextrow = scan indent lines (sr + 1)
 
   -- No init or first :: rest for add missing case
   let (edits, rest) = doFirst inPlace cons
 
   let phead = pack head
-  let fc' = MkFC uri (MkBounds (sr + 1) 0 (sr + 1) 0)
+  let fc' = MkFC uri (MkBounds nextrow 0 nextrow 0)
   let srest =
-    if isEq
-      then joinBy "" $ map (\ap => phead ++ ap ++ before ++ "= ?\n") rest
-      else joinBy "" $ map (\ap => "  | \{pack head}\{ap}\{before}=> ?\n") rest
+    case splitKind of
+      EqSplit => joinBy "" $ map (\ap => phead ++ ap ++ before ++ "= ?\n") rest
+      FatArrowSplit => joinBy "" $ map (\ap => phead ++ ap ++ before ++ "=> ?\n") rest
+      MonadSplit => joinBy "" $ map (\ap => "  | \{pack head}\{ap}\{before}=> ?\n") rest
 
   putStrLn "Split \{show line} HD '\{show head}' TL '\{show tail}'"
   putStrLn srest
@@ -135,6 +144,15 @@ makeEdits fc@(MkFC uri (MkBounds sr sc er ec)) names inPlace = do
   putStrLn "edits \{debugStr edits}"
   pure edits
   where
+    getIndent : Int → List Char → Int
+    getIndent acc (' ' :: rest) = getIndent (1 + acc) rest
+    getIndent acc _ = acc
+
+    scan : Int → List String → Int → Int
+    scan indent lines row =
+      let x = getIndent 0 $ unpack $ fromMaybe "" $ getAt' row lines in
+      if x <= indent then row else scan indent lines (row + 1)
+
     doFirst : Bool → List String → (List FileEdit × List String)
     doFirst True (first :: rest) = (MkEdit fc first :: Nil, rest)
     doFirst _ cons = (Nil, cons)
@@ -163,13 +181,83 @@ posInFC : Int → Int → FC → Bool
 -- FIXME ec + 1 again...
 posInFC row col (MkFC _ (MkBounds sr sc er ec)) = (sr <= row && row <= er) && (sc <= col && col <= ec + 1)
 
+getHole : ModContext → Int → Int → Maybe MetaEntry
+getHole mod row col =
+  find isUserMeta $ listValues mod.modMetaCtx.metas
+  where
+    isUserMeta : MetaEntry → Bool
+    isUserMeta (Unsolved fc _ _ _ User _) = posInFC row col fc
+    isUserMeta _ = False
+
+introActions : Maybe MetaEntry → M (List CodeAction)
+introActions (Just $ Unsolved fc qn ctx vty User constraints) =
+  catchError (do
+    -- Are there ever any constraints?
+    top <- getTop
+    vty <- forceMeta vty
+    putStrLn "intros for \{show vty}"
+    case vty of
+      VPi _ nm Explicit _ a b => do
+        let str = "(\\ \{nm} => ?)"
+        pure $ Intro str (MkEdit fc str) :: Nil
+      _ => do
+        -- Prelude.Nat not a vref?
+        -- also need to handle pi types
+        cons <- getConstructors ctx fc vty
+        putStrLn "constructors \{show cons}"
+        pure $ map makeEdit cons
+  ) $ \ err => do
+      putStrLn "Got error in introActions:"
+      putStrLn $ showError "" err
+      pure Nil
+  where
+    introDCon : QName × Int × Tm → List String
+    introDCon (QN _ nm, _, tm) = go (Lin :< nm) tm
+      where
+        go : SnocList String → Tm → List String
+        go acc (Pi _ nm Explicit _ _ u) = go (acc :< "?") u
+        go acc (Pi _ _ _ _ _ u) = go acc u
+        go acc _ = acc <>> Nil
+
+    makeEdit : (QName × Int × Tm) → CodeAction
+    makeEdit con@(QN _ nm, _, _) =
+      let str = unwords $ resugarOper $ introDCon con
+      in Intro str $ MkEdit fc $ str
+
+introActions _ = pure Nil
+
+errorActions : Int → Int → Error → M (List CodeAction)
+errorActions row col err = do
+  let (ENotFound fc nm) = err | _ => pure Nil
+  let (True) = posInFC row col fc | _ => pure Nil
+  top <- getTop
+  let mods = map (\e => e.name.qns) $ lookupAll nm top
+  case mods of
+    Nil => pure Nil
+    _ => do
+      top <- getTop
+      let row = getInsertRow 0 1 $ split top.currentMod.modSource "\n"
+      let fc = MkFC fc.file (MkBounds row 0 row 0)
+      pure $ map (\nm => ImportAction nm (MkEdit fc "import \{nm}\n")) mods
+  where
+    getInsertRow : Int → Int → List String → Int
+    getInsertRow row cur Nil = row
+    getInsertRow row cur (l :: ls) =
+      let row =  ite (isPrefixOf "module" l || isPrefixOf "import" l) cur row
+      in getInsertRow row (cur + 1) ls
+
 getActions : FileSource → String → Int → Int → M (List CodeAction)
 getActions repo modns row col = do
-  mod <- switchModule repo modns
+  Just mod <- switchModule repo modns | _ => pure Nil
   top <- getTop
-  let xx = filter (posInFC row col ∘ getFC) top.currentMod.modInfos
-  putStrLn "Filter got \{show $ length' xx}"
-  go Nil $ xx
+  let infos = filter (posInFC row col ∘ getFC) top.currentMod.modInfos
+  putStrLn "Filter got \{show $ length' infos}"
+  actions <- go Nil $ infos
+  let hole = getHole mod row col
+  putStrLn "Hole \{debugStr hole}"
+  intros <- introActions $ getHole mod row col
+  eactions <- join <$> traverse (errorActions row col) mod.modErrors
+  pure $ actions ++ intros ++ eactions
   where
     getAction : EditorInfo → M (Maybe CodeAction)
     getAction (CaseSplit fc ctx nm scty) = getCaseSplit row col fc ctx nm scty

src/LSP.newt

@@ -13,8 +13,6 @@ import Data.SortedMap
 import Data.IORef
 import Node
 import Commands
-import Data.List1
-import Lib.Prettier
 import Lib.ProcessDecl
 
 pfunc js_castArray : Array JSObject → JSObject := `x => x`
@@ -143,6 +141,16 @@ codeActionInfo uri line col = unsafePerformIO $ do
         $ ("title", JsonStr "Case split")
         :: ("edit", (single "changes" $ single uri $ JsonArray $ map editToJson edits))
         :: Nil
+    actionToJson (Intro name edit) =
+      JsonObj
+        $ ("title", JsonStr "Intro \{name}")
+        :: ("edit", (single "changes" $ single uri $ JsonArray $ editToJson edit :: Nil))
+        :: Nil
+    actionToJson (ImportAction name edit) =
+      JsonObj
+        $ ("title", JsonStr "Import \{name}")
+        :: ("edit", (single "changes" $ single uri $ JsonArray $ editToJson edit :: Nil))
+        :: Nil
     actionToJson (AddMissingAction edits) =
       JsonObj
         $ ("title", JsonStr "Add missing cases")
@@ -150,11 +158,11 @@ codeActionInfo uri line col = unsafePerformIO $ do
         :: Nil
 
 errorToDiag : Error -> Json
-errorToDiag (E fc msg) =
+errorToDiag err =
   JsonObj
     $  ("severity", JsonInt 1)
-    :: ("range", fcToRange fc)
-    :: ("message", JsonStr msg)
+    :: ("range", fcToRange (getFC err))
+    :: ("message", JsonStr (errorMsg err))
     :: ("source", JsonStr "newt") -- what is this key for?
     :: Nil
 -- These shouldn't escape
@@ -194,7 +202,8 @@ checkFile fn = unsafePerformIO $ do
         else pure MkUnit
     (Right (top, json)) <- (do
         putStrLn "processModule"
-        _ <- switchModule lspFileSource modName
+        mod <- processModule emptyFC lspFileSource Nil modName
+        modifyTop [ currentMod := mod; ops := mod.modOps ]
 
         -- pull out errors and infos
         top <- getTop

src/Lib/Common.newt

@@ -142,11 +142,10 @@ emptyFC' : String → FC
 emptyFC' fn = MkFC fn (MkBounds 0 0 0 0)
 
 -- Using a String instead of List String for the module shaved about 16% of compile time...
-data QName : U where
-  QN : String -> String -> QName
-
-.baseName : QName → String
-(QN _ name).baseName = name
+record QName where
+  constructor QN
+  qns : String
+  baseName : String
 
 instance Eq QName where
   -- `if` gets us short circuit behavior, idris has a lazy `&&`
@@ -159,34 +158,39 @@ instance Show QName where
 instance Ord QName where
   compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns'
 
+-- I'll want to get Context / Val in some of these
+-- and a pretty printer in the monad
 data Error
   = E FC String
+  | ENotFound FC String
   | Postpone FC QName String
 
 instance Show FC where
   show (MkFC file (MkBounds l c el ec)) = "\{file}:\{show $ l + 1}:\{show $ c + 1}--\{show $ el + 1}:\{show $ ec + 1}"
 
-showError : String -> Error -> String
-showError src (E fc msg) = "ERROR at \{show fc}: \{msg}\n" ++ go 0 (lines src)
+instance HasFC Error where
+  getFC (E x str) = x
+  getFC (ENotFound x _) = x
+  getFC (Postpone x k str) = x
+
+errorMsg : Error -> String
+errorMsg (E x str) = str
+errorMsg (ENotFound x nm) = "\{nm} not in scope"
+errorMsg (Postpone x k str) = str
+
+showError : (src : String) -> Error -> String
+showError src err =
+  let fc = getFC err
+  in "ERROR at \{show $ getFC err}: \{errorMsg err}\n" ++ go fc 0 (lines src)
   where
-    go : Int -> List String -> String
-    go l Nil = ""
-    go l (x :: xs) =
+    go : FC → Int → List String → String
+    go fc l Nil = ""
+    go fc l (x :: xs) =
       if l == fcLine fc then
         let width = fc.bnds.endCol - fc.bnds.startCol in
         "  \{x}\n  \{replicate (cast $ fcCol fc) ' '}\{replicate (cast width) '^'}\n"
-      else if fcLine fc - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
-      else go (l + 1) xs
-showError src (Postpone fc ix msg) = "ERROR at \{show fc}: Postpone \{show ix} \{msg}\n" ++ go 0 (lines src)
-  where
-    go : Int -> List String -> String
-    go l Nil = ""
-    go l (x :: xs) =
-      if l == fcLine fc then
-        "  \{x}\n  \{replicate (cast $ fcCol fc) ' '}^\n"
-      else if fcLine fc - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
-      else go (l + 1) xs
-
+      else if fcLine fc - 3 < l then "  " ++ x ++ "\n" ++ go fc (l + 1) xs
+      else go fc (l + 1) xs
 
 data Fixity = InfixL | InfixR | Infix
 

src/Lib/Elab.newt

@@ -999,12 +999,11 @@ mkPat (tm, icit) = do
                   pure $ PatCon (getFC tm) icit name bpat Nothing
                 -- This fires when a global is shadowed by a pattern var
                 -- Just _ => error (getFC tm) "\{show nm} is not a data constructor"
-                _ => case b of
-                    -- TODO maybe check case?
-                    Nil =>
-                      if isUpperName nm
+                _ => if isUpperName nm
+                        -- This is not entirely accurate - it could be a function def
                         then error (getFC tm) "\{nm} not in scope"
-                        else pure $ PatVar fc icit nm
+                        else case b of
+                          Nil => pure $ PatVar fc icit nm
                           _ => error (getFC tm) "patvar applied to args"
     ((RImplicit fc), Nil) => pure $ PatWild fc icit
     ((RImplicit fc), _) => error fc "implicit pat can't be applied to arguments"
@@ -1486,9 +1485,10 @@ check ctx tm ty = do
                 pure $ Lam fc nm' icit rig sc
               else
                 error fc "Icity issue checking \{show t} at \{show ty}"
-    (t@(RLam _ (BI fc nm icit quant) tm), ty) => do
+    (t@(RLam fc (BI _ nm icit quant) tm), ty) => do
               pty <- prvalCtx ty
-              error fc "Expected \{pty}, got pi type"
+              -- TODO I'm hitting this with an unsolved meta
+              error fc "Expected \{pty}, got a function"
 
     (RLet fc nm ty v sc, rty) => do
       ty' <- check ctx ty (VU emptyFC)
@@ -1503,7 +1503,7 @@ check ctx tm ty = do
 
     (tm, ty@(VPi fc nm' Implicit rig a b)) => do
       let names = map fst ctx.types
-      debug $ \ _ => "XXX edge case add implicit lambda {\{nm'} : \{show a}} to \{show tm} "
+      debug $ \ _ => "elab.insert: Add implicit lambda {\{nm'} : \{show a}} to \{show tm} "
       let var = VVar fc (length' ctx.env) Lin
       ty' <- b $$ var
       debugM $ do
@@ -1513,13 +1513,12 @@ check ctx tm ty = do
       pure $ Lam (getFC tm) nm' Implicit rig sc
 
     (tm, ty@(VPi fc nm' Auto rig a b)) => do
-      let names = map fst ctx.types
-      debug $ \ _ => "XXX edge case add auto lambda {\{nm'} : \{show a}} to \{show tm} "
+      debug $ \ _ => "elab.insert: Add auto lambda {\{nm'} : \{show a}} to \{show tm}"
       let var = VVar fc (length' ctx.env) Lin
       ty' <- b $$ var
       debugM $ do
         pty' <- prvalCtx {{(extend ctx nm' a)}} ty'
-        pure "XXX ty' is \{pty'}"
+        pure "elab.insert: ty' is \{pty'}"
       sc <- check (extend ctx nm' a) tm ty'
       pure $ Lam (getFC tm) nm' Auto rig sc
 
@@ -1536,9 +1535,6 @@ infer ctx tm@(RUpdateRec fc _ _) = error fc "I can't infer record updates"
 
 infer ctx (RVar fc nm) = go 0 ctx.types
   where
-    entryNS : TopEntry → String
-    entryNS (MkEntry fc (QN ns _) _ _ _) = ns
-
     go : Int -> List (String × Val)  -> M (Tm × Val)
     go i Nil = do
       top <- getTop
@@ -1547,13 +1543,8 @@ infer ctx (RVar fc nm) = go 0 ctx.types
           debug $ \ _ => "lookup \{show name} as \{show def}"
           vty <- eval Nil ty
           pure (Ref fc name, vty)
-        Nothing => do
-          let mods = map entryNS $ lookupAll nm top
-          let extra = case mods of
-            Nil => ""
-            -- For the benefit of the editor, but only sees transitive modules
-            _ => ", try importing: \{joinBy ", " mods}"
-          error fc "\{show nm} not in scope\{extra}"
+        -- Can we soften this without introducing a meta?
+        Nothing => throwError $ ENotFound fc nm
     go i ((x, ty) :: xs) = if x == nm then pure (Bnd fc i, ty)
       else go (i + 1) xs
 

src/Lib/Eval.newt

@@ -268,28 +268,18 @@ prvalCtx {{ctx}} v = do
   tm <- quote ctx.lvl v
   pure $ render 90 $ pprint (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.
+-- 'zonk' is substituting metas _and_ doing inlining
 
--- 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.)
+-- It is a flavor of eval, maybe we could combine them with some flags
+-- to control what gets reduced.
 
 zonk : TopContext -> Int -> Env -> Tm -> M Tm
 
 zonkBind : TopContext -> Int -> Env -> Tm -> M Tm
 zonkBind top l env tm = zonk top (1 + l) (VVar (getFC tm) l Lin :: env) tm
 
--- I don't know if app needs an FC...
-
+-- REVIEW FC might be dicey here
 appSpine : Tm -> List Tm -> Tm
 appSpine t Nil = t
 appSpine t (x :: xs) = appSpine (App (getFC t) t x) xs

src/Lib/Parser.newt

@@ -311,14 +311,16 @@ pLamArg = impArg <|> autoArg <|> expArg
 lamExpr : Parser Raw
 lamExpr = do
   pos <- getPos
+  (fc, args, scope) <- withFC $ do
     keyword "\\" <|> keyword "λ"
     args <- some $ addPos pLamArg
     keyword "=>"
     scope <- typeExpr
-  pure $ foldr mkLam scope args
+    pure (args, scope)
+  pure $ foldr (mkLam fc) scope args
   where
-    mkLam : FC × Icit × Name × Maybe Raw → Raw → Raw
-    mkLam (fc, icit, name, ty) sc = RLam fc (BI fc name icit Many) sc
+    mkLam : FC → FC × Icit × Name × Maybe Raw → Raw → Raw
+    mkLam fc (nfc, icit, name, ty) sc = RLam fc (BI nfc name icit Many) sc
 
 
 caseAlt : Parser RCaseAlt
@@ -566,10 +568,11 @@ parseDef = do
   nm <- getName t
   Just _ <- optional $ keyword "="
     -- impossible clause
+    -- TODO we should require outdent
     | Nothing => pure $ FunDef fc nm ((t,Nothing) :: Nil)
+  -- TODO could we recover and keep the LHS?
   body <- typeExpr
-  wfc <- getPos
-  w <- optional $ do
+  (wfc, w) <- withFC $ optional $ do
     keyword "where"
     startBlock $ manySame $ (parseSig <|> parseDef)
   let body = maybe body (\ decls => RWhere wfc decls body) w

src/Lib/Types.newt

@@ -570,13 +570,6 @@ debugM x = logM 2 x
 instance Show Context where
   show ctx = "Context \{show $ map fst $ ctx.types}"
 
-errorMsg : Error -> String
-errorMsg (E x str) = str
-errorMsg (Postpone x k str) = str
-
-instance HasFC Error where
-  getFC (E x str) = x
-  getFC (Postpone x k str) = x
 
 error : ∀ a. FC -> String -> M a
 error fc msg = throwError $ E fc msg

tests/aside/InferIssue.newt

@@ -0,0 +1,11 @@
+module InferIssue
+
+-- inline prelude to reduce log size
+infixr 8 _×_
+infixr 2 _,_
+data a × b = (a,b)
+data Nat = Z | S Nat
+
+-- unification error because meta isn't solved yet
+foo : Nat → (Nat × (Nat → Nat))
+foo x = (Z , (\ x => 10))