0 | module Idris.REPL

   2 | import Compiler.Common

   3 | import Compiler.Inline

   5 | import Core.Case.CaseTree

   6 | import Core.CompileExpr

   7 | import Core.CompileExpr.Pretty

   8 | import Core.Context.Pretty

   9 | import Core.Directory

  10 | import Core.Env

  11 | import Core.LinearCheck

  12 | import Core.Metadata

  13 | import Core.TT.Views

  14 | import Core.Termination

  15 | import Core.Unify

  16 | import Core.Value

  18 | import Core.SchemeEval

  20 | import Parser.Unlit

  22 | import Idris.CommandLine

  23 | import Idris.Desugar

  24 | import Idris.Doc.Display

  25 | import Idris.Doc.String

  26 | import Idris.Error

  27 | import Idris.IDEMode.CaseSplit

  28 | import Idris.IDEMode.Commands

  29 | import Idris.IDEMode.MakeClause

  30 | import Idris.IDEMode.Holes

  31 | import Idris.ModTree

  32 | import Idris.Parser

  33 | import Idris.Pretty

  34 | import Idris.ProcessIdr

  35 | import Idris.Resugar

  36 | import Idris.Syntax

  37 | import Idris.Version

  39 | import public Idris.REPL.Common

  40 | import Idris.REPL.FuzzySearch

  42 | import TTImp.TTImp.Functor

  43 | import TTImp.Elab

  44 | import TTImp.Elab.Check

  45 | import TTImp.Elab.Local

  46 | import TTImp.Interactive.CaseSplit

  47 | import TTImp.Interactive.ExprSearch

  48 | import TTImp.Interactive.GenerateDef

  49 | import TTImp.Interactive.Intro

  50 | import TTImp.Interactive.MakeLemma

  51 | import TTImp.TTImp

  52 | import TTImp.Unelab

  53 | import TTImp.Utils

  54 | import TTImp.BindImplicits

  55 | import TTImp.ProcessDecls

  57 | import Data.Maybe

  58 | import Libraries.Data.NatSet

  59 | import Libraries.Data.NameMap

  60 | import Libraries.Data.PosMap

  61 | import Libraries.Data.String as L

  62 | import Data.Stream

  63 | import Data.String

  64 | import Libraries.Data.SparseMatrix

  65 | import Libraries.Data.Tap

  66 | import Libraries.Data.WithDefault

  67 | import Libraries.Utils.Path

  68 | import Libraries.System.Directory.Tree

  70 | import System

  71 | import System.File

  73 | %default covering

  77 | showInfo : {auto c : Ref Ctxt Defs} ->

  78 |            (Name, Int, GlobalDef) -> Core ()

  79 | showInfo (n, idx, d)

  80 |     = do coreLift_ $ putStrLn (show (fullname d) ++ " ==> " ++

  81 |                               show !(toFullNames (definition d)))

  82 |          coreLift_ $ putStrLn (show (multiplicity d))

  83 |          coreLift_ $ putStrLn ("Erasable args: " ++ show (eraseArgs d))

  84 |          coreLift_ $ putStrLn ("Detaggable arg types: " ++ show (safeErase d))

  85 |          coreLift_ $ putStrLn ("Specialise args: " ++ show (specArgs d))

  86 |          coreLift_ $ putStrLn ("Inferrable args: " ++ show (inferrable d))

  87 |          whenJust (compexpr d) $ \ expr =>

  88 |            coreLift_ $ putStrLn ("Compiled: " ++ show expr)

  89 |          coreLift_ $ putStrLn ("Refers to: " ++

  90 |                                show !(traverse getFullName (keys (refersTo d))))

  91 |          coreLift_ $ putStrLn ("Refers to (runtime): " ++

  92 |                                show !(traverse getFullName (keys (refersToRuntime d))))

  93 |          coreLift_ $ putStrLn ("Flags: " ++ show (flags d))

  94 |          when (not (isNil (sizeChange d))) $

  95 |             let scinfo = map (\s => show (fnCall s) ++ ": " ++

  96 |                                     show (fnArgs s)) !(traverse toFullNames (sizeChange d)) in

  97 |                 coreLift_ $ putStrLn $

  98 |                         "Size change: " ++ showSep ", " scinfo

 100 | prettyInfo : {auto c : Ref Ctxt Defs} ->

 101 |              {auto s : Ref Syn SyntaxInfo} ->

 102 |              (Name, Int, GlobalDef) -> Core (Doc IdrisDocAnn)

 103 | prettyInfo (n, idx, d)

 104 |     = do let nm = fullname d

 105 |          def <- toFullNames (definition d)

 106 |          referCT <- traverse getFullName (keys (refersTo d))

 107 |          referRT <- traverse getFullName (keys (refersToRuntime d))

 108 |          schanges <- traverse toFullNames $ sizeChange d

 109 |          pp <- getPPrint

 110 |          setPPrint ({ showMachineNames := True } pp)

 111 |          def <- Resugared.prettyDef def

 112 |          setPPrint ({ showMachineNames := showMachineNames pp } pp)

 113 |          pure $ vcat $

 114 |            [ reAnnotate Syntax (prettyRig $ multiplicity d) <+> showCategory Syntax d (pretty0 nm)

 115 |            , def

 116 |            ] ++

 117 |            catMaybes

 118 |            [ (\ args => header "Erasable args" <++> byShow args) <$> ifNotEmpty (eraseArgs d)

 119 |            , (\ args => header "Detaggable arg types" <++> byShow args) <$> ifNotEmpty (safeErase d)

 120 |            , (\ args => header "Specialise args" <++> byShow args) <$> ifNotEmpty (specArgs d)

 121 |            , (\ args => header "Inferrable args" <++> byShow args) <$> ifNotEmpty (inferrable d)

 122 |            , (\ expr => header "Compiled" <++> pretty expr) <$> compexpr d

 123 |            , (\ nms  => header "Refers to" <++> enum pretty0 nms) <$> ifNotNull referCT

 124 |            , (\ nms  => header "Refers to (runtime)" <++> enum pretty0 nms) <$> ifNotNull referRT

 125 |            , (\ flgs => header "Flags" <++> enum byShow flgs) <$> ifNotNull (flags d)

 126 |            , (\ sz   => header "Size change" <+> hardline <+> indent 2 (displayChg sz)) <$> ifNotNull schanges

 127 |            ]

 129 |   where

 130 |     ifNotNull : List a -> Maybe (List a)

 131 |     ifNotNull xs = xs <$ guard (not $ null xs)

 133 |     ifNotEmpty : NatSet -> Maybe NatSet

 134 |     ifNotEmpty xs = xs <$ guard (not $ isEmpty xs)

 136 |     enum : (a -> Doc IdrisDocAnn) -> List a -> Doc IdrisDocAnn

 137 |     enum p xs = hsep $ punctuate "," $ p <$> xs

 139 |     enumLine : (a -> Doc IdrisDocAnn) -> List a -> Doc IdrisDocAnn

 140 |     enumLine p xs = hcat $ punctuate hardline $ p <$> xs

 142 |     displayChg : List SCCall -> Doc IdrisDocAnn

 143 |     displayChg sz =

 144 |       let scinfo = \s => pretty0 (fnCall s) <+> ":" <+> hardline <+> cast (prettyTable "r" "l" 1 (fnArgs s)) in

 145 |       enumLine scinfo sz

 147 | getEnvTerm : {vars : _} ->

 148 |              List Name -> Env Term vars -> Term vars ->

 149 |              (vars' ** (Env Term vars', Term vars'))

 150 | getEnvTerm (n :: ns) env (Bind fc x b sc)

 151 |     = if n == x

 152 |          then getEnvTerm ns (b :: env) sc

 153 |          else (_ ** (env, Bind fc x b sc))

 154 | getEnvTerm _ env tm = (_ ** (env, tm))

 156 | displayPatTerm : {auto c : Ref Ctxt Defs} ->

 157 |                  {auto s : Ref Syn SyntaxInfo} ->

 158 |                  Defs -> ClosedTerm ->

 159 |                  Core String

 160 | displayPatTerm defs tm

 161 |     = do ptm <- resugarNoPatvars Env.empty !(normaliseHoles defs Env.empty tm)

 162 |          pure (show ptm)

 164 | setOpt : {auto c : Ref Ctxt Defs} ->

 165 |          {auto o : Ref ROpts REPLOpts} ->

 166 |          REPLOpt -> Core ()

 167 | setOpt (ShowImplicits t)

 168 |     = updatePPrint { showImplicits := t }

 169 | setOpt (ShowNamespace t)

 170 |     = updatePPrint { fullNamespace := t }

 171 | setOpt (ShowMachineNames t)

 172 |     = updatePPrint { showMachineNames := t }

 173 | setOpt (ShowTypes t)

 174 |     = update ROpts { showTypes := t }

 175 | setOpt (EvalMode m)

 176 |     = update ROpts { evalMode := m }

 177 | setOpt (Editor e)

 178 |     = update ROpts { editor := e }

 179 | setOpt (CG e)

 180 |     = do defs <- get Ctxt

 181 |          case getCG (options defs) e of

 182 |             Just cg => setCG cg

 183 |             Nothing => iputStrLn (reflow "No such code generator available")

 184 | setOpt (Profile t)

 185 |     = do pp <- getSession

 186 |          setSession ({ profile := t } pp)

 187 | setOpt (EvalTiming t)

 188 |     = setEvalTiming t

 190 | getOptions : {auto c : Ref Ctxt Defs} ->

 191 |          {auto o : Ref ROpts REPLOpts} ->

 192 |          Core (List REPLOpt)

 193 | getOptions = do

 194 |   pp <- getPPrint

 195 |   opts <- get ROpts

 196 |   pure $ [ ShowImplicits (showImplicits pp), ShowMachineNames (showMachineNames pp)

 197 |          , ShowNamespace (fullNamespace pp)

 198 |          , ShowTypes (showTypes opts), EvalMode (evalMode opts)

 199 |          , Editor (editor opts)

 200 |          ]

 202 | anyAt : (a -> Bool) -> a -> b -> Bool

 203 | anyAt p loc _ = p loc

 205 | printClause : {auto c : Ref Ctxt Defs} ->

 206 |               {auto s : Ref Syn SyntaxInfo} ->

 207 |               Maybe String -> Nat -> ImpClause ->

 208 |               Core String

 209 | printClause l i (PatClause _ lhsraw rhsraw)

 210 |     = do lhs <- pterm $ map defaultKindedName lhsraw -- hack

 211 |          rhs <- pterm $ map defaultKindedName rhsraw -- hack

 212 |          pure (relit l (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs))

 213 | printClause l i (WithClause _ lhsraw rig wvraw prf flags csraw)

 214 |     = do lhs <- pterm $ map defaultKindedName lhsraw -- hack

 215 |          wval <- pterm $ map defaultKindedName wvraw -- hack

 216 |          cs <- traverse (printClause l (i + 2)) csraw

 217 |          pure (relit l (pack (replicate i ' ')

 218 |                 ++ show lhs

 219 |                 ++ " with " ++ showCount rig ++ "(" ++ show wval ++ ")"

 220 |                    -- TODO: remove `the` after fix idris-lang/Idris2#3418

 221 |                 ++ maybe "" (the (_ -> _) $ \(rg, nm) => " proof " ++ showCount rg ++ show nm) prf

 222 |                 ++ "\n")

 223 |                ++ showSep "\n" cs)

 224 | printClause l i (ImpossibleClause _ lhsraw)

 225 |     = do lhs <- pterm $ map defaultKindedName lhsraw -- hack

 226 |          pure (relit l (pack (replicate i ' ') ++ show lhs ++ " impossible"))

 229 | lookupDefTyName : Name -> Context ->

 230 |                   Core (List (Name, Int, (Def, ClosedTerm)))

 231 | lookupDefTyName = lookupNameBy (\g => (definition g, type g))

 233 | updateFile : {auto r : Ref ROpts REPLOpts} ->

 234 |              (List String -> List String) -> Core EditResult

 235 | updateFile update

 236 |     = do opts <- get ROpts

 237 |          let Just f = mainfile opts

 238 |              | Nothing => pure (DisplayEdit emptyDoc) -- no file, nothing to do

 239 |          Right content <- coreLift $ readFile f

 240 |                | Left err => throw (FileErr f err)

 241 |          coreLift_ $ writeFile (f ++ "~") content

 242 |          coreLift_ $ writeFile f (unlines (update (lines content)))

 243 |          pure (DisplayEdit emptyDoc)

 245 | addClause : String -> Nat -> List String -> List String

 246 | addClause c Z [] = L.rtrim c :: []

 247 | addClause c Z (x :: xs)

 248 |     = if all isSpace (unpack x)

 249 |          then L.rtrim c :: x :: xs

 250 |          else x :: addClause c Z xs

 251 | addClause c (S k) (x :: xs) = x :: addClause c k xs

 252 | addClause c (S k) [] = [c]

 254 | caseSplit : String -> Nat -> List String -> List String

 255 | caseSplit c Z (x :: xs) = L.rtrim c :: xs

 256 | caseSplit c (S k) (x :: xs) = x :: caseSplit c k xs

 257 | caseSplit c _ [] = [c]

 259 | proofSearch : Name -> String -> Nat -> List String -> List String

 260 | proofSearch n res Z (x :: xs) = replaceStr ("?" ++ show n) res x :: xs

 261 |   where

 262 |     replaceStr : String -> String -> String -> String

 263 |     replaceStr rep new "" = ""

 264 |     replaceStr rep new str

 265 |         = if isPrefixOf rep str

 266 |              then new ++ pack (drop (length rep) (unpack str))

 267 |              else assert_total $ strCons (prim__strHead str)

 268 |                           (replaceStr rep new (prim__strTail str))

 269 | proofSearch n res (S k) (x :: xs) = x :: proofSearch n res k xs

 270 | proofSearch n res _ [] = []

 272 | addMadeLemma : Maybe String -> Name -> String -> String -> Nat -> List String -> List String

 273 | addMadeLemma lit n ty app line content

 274 |     = addApp lit line [] (proofSearch n app line content)

 275 |   where

 276 |     -- Put n : ty in the first blank line

 277 |     insertInBlank : Maybe String -> List String -> List String

 278 |     insertInBlank lit [] = [relit lit $ show n ++ " : " ++ ty ++ "\n"]

 279 |     insertInBlank lit (x :: xs)

 280 |         = if trim x == ""

 281 |              then ("\n" ++ (relit lit $ show n ++ " : " ++ ty ++ "\n")) :: xs

 282 |              else x :: insertInBlank lit xs

 284 |     addApp : Maybe String -> Nat -> List String -> List String -> List String

 285 |     addApp lit Z acc rest = reverse (insertInBlank lit acc) ++ rest

 286 |     addApp lit (S k) acc (x :: xs) = addApp lit k (x :: acc) xs

 287 |     addApp _ (S k) acc [] = reverse acc

 290 | addMadeCase : Maybe String -> List String -> Nat -> List String -> List String

 291 | addMadeCase lit wapp line content

 292 |     = addW line [] content

 293 |   where

 294 |     addW : Nat -> List String -> List String -> List String

 295 |     addW Z acc (_ :: rest) = reverse acc ++ map (relit lit) wapp ++ rest

 296 |     addW Z acc [] = [] -- shouldn't happen!

 297 |     addW (S k) acc (x :: xs) = addW k (x :: acc) xs

 298 |     addW (S k) acc [] = reverse acc

 300 | nextProofSearch : {auto c : Ref Ctxt Defs} ->

 301 |                   {auto u : Ref UST UState} ->

 302 |                   {auto o : Ref ROpts REPLOpts} ->

 303 |                   Core (Maybe (Name, RawImp))

 305 |     = do opts <- get ROpts

 306 |          let Just (n, res) = psResult opts

 307 |               | Nothing => pure Nothing

 308 |          Just (res, next) <- nextResult res

 309 |               | Nothing =>

 310 |                     do put ROpts ({ psResult := Nothing } opts)

 311 |                        pure Nothing

 312 |          put ROpts ({ psResult := Just (n, next) } opts)

 313 |          pure (Just (n, res))

 315 | nextGenDef : {auto c : Ref Ctxt Defs} ->

 316 |              {auto u : Ref UST UState} ->

 317 |              {auto o : Ref ROpts REPLOpts} ->

 318 |              (reject : Nat) ->

 319 |              Core (Maybe (Int, (FC, List ImpClause)))

 320 | nextGenDef reject

 321 |     = do opts <- get ROpts

 322 |          let Just (line, res) = gdResult opts

 323 |               | Nothing => pure Nothing

 324 |          Just (res, next) <- nextResult res

 325 |               | Nothing =>

 326 |                     do put ROpts ({ gdResult := Nothing } opts)

 327 |                        pure Nothing

 328 |          put ROpts ({ gdResult := Just (line, next) } opts)

 329 |          case reject of

 330 |               Z => pure (Just (line, res))

 331 |               S k => nextGenDef k

 333 | dropLams : Nat -> RawImp' nm -> RawImp' nm

 334 | dropLams Z tm = tm

 335 | dropLams (S k) (ILam _ _ _ _ _ sc) = dropLams k sc

 336 | dropLams _ tm = tm

 338 | dropLamsTm : {vars : _} ->

 339 |              Nat -> Env Term vars -> Term vars ->

 340 |              (vars' ** (Env Term vars', Term vars'))

 341 | dropLamsTm Z env tm = (_ ** (env, tm))

 342 | dropLamsTm (S k) env (Bind _ _ b sc) = dropLamsTm k (b :: env) sc

 343 | dropLamsTm _ env tm = (_ ** (env, tm))

 345 | findInTree : FilePos -> Name -> PosMap (NonEmptyFC, Name) -> Maybe Name

 346 | findInTree p hint m

 347 |   = map snd $ head'

 348 |   $ sortBy (cmp `on` measure)

 349 |   $ filter match

 350 |   $ searchPos p m

 352 |   where

 353 |     cmp : FileRange -> FileRange -> Ordering

 354 |     cmp ((sr1, sc1), (er1, ec1)) ((sr2, sc2), (er2, ec2)) =

 355 |       compare (er1 - sr1, ec1 - sc1) (er2 - sr2, ec2 - sc2)

 357 |     checkAsNamespace : String -> Name -> Bool

 358 |     checkAsNamespace i (NS ns' n) = i `isInPathOf` ns'

 359 |     checkAsNamespace _ _ = False

 361 |     startsWithUpper : String -> Bool

 362 |     startsWithUpper str = case strM str of

 363 |        StrNil => False

 364 |        StrCons c _ => isUpper c || c > chr 160

 366 |     matchingRoots : Name -> Name -> Bool

 367 |     matchingRoots = (==) `on` nameRoot

 369 |     checkCandidate : Name -> Bool

 370 |     checkCandidate cand = matchingRoots hint cand || case hint of

 371 |       -- a basic user name: may actually be e.g. the `B` part of `A.B.C.val`

 372 |       UN (Basic n) => startsWithUpper n && checkAsNamespace n cand

 373 |       _ => False

 375 |     match : (NonEmptyFC, Name) -> Bool

 376 |     match (_, n) = matches hint n && checkCandidate n

 378 | record TermWithType (vars : Scope) where

 379 |   constructor WithType

 380 |   termOf : Term vars

 381 |   typeOf : Term vars

 383 | getItDecls :

 384 |     {auto o : Ref ROpts REPLOpts} ->

 385 |     Core (List ImpDecl)

 387 |     = do opts <- get ROpts

 388 |          case evalResultName opts of

 389 |             Nothing => pure []

 390 |             Just n =>

 391 |               let it = UN $ Basic "it" in

 392 |               pure [ IClaim

 393 |                        (MkFCVal replFC $ MkIClaimData top Private []

 394 |                                        $ Mk [replFC, NoFC it] (Implicit replFC False))

 395 |                   , IDef replFC it [PatClause replFC (IVar replFC it) (IVar replFC n)]]

 398 | inferAndElab :

 399 |   {vars : _} ->

 400 |   {auto c : Ref Ctxt Defs} ->

 401 |   {auto u : Ref UST UState} ->

 402 |   {auto s : Ref Syn SyntaxInfo} ->

 403 |   {auto m : Ref MD Metadata} ->

 404 |   {auto o : Ref ROpts REPLOpts} ->

 405 |   ElabMode ->

 406 |   PTerm ->

 407 |   Env Term vars ->

 408 |   Core (TermWithType vars)

 409 | inferAndElab emode itm env

 410 |   = do ttimp <- desugar AnyExpr (toList vars) itm

 411 |        let ttimpWithIt = ILocal replFC !getItDecls ttimp

 412 |        inidx <- resolveName (UN $ Basic "[input]")

 413 |        -- a TMP HACK to prioritise list syntax for List: hide

 414 |        -- foreign argument lists. TODO: once the new FFI is fully

 415 |        -- up and running we won't need this. Also, if we add

 416 |        -- 'with' disambiguation we can use that instead.

 417 |        catch (do hide replFC (NS primIONS (UN $ Basic "::"))

 418 |                  hide replFC (NS primIONS (UN $ Basic "Nil")))

 419 |              (\err => pure ())

 420 |        (tm , gty) <- elabTerm inidx emode [] (MkNested []) env ttimpWithIt Nothing

 421 |        ty <- getTerm gty

 422 |        pure (tm `WithType` ty)

 424 | processEdit : {auto c : Ref Ctxt Defs} ->

 425 |               {auto u : Ref UST UState} ->

 426 |               {auto s : Ref Syn SyntaxInfo} ->

 427 |               {auto m : Ref MD Metadata} ->

 428 |               {auto o : Ref ROpts REPLOpts} ->

 429 |               EditCmd -> Core EditResult

 430 | processEdit (TypeAt line col name)

 431 |     = do defs <- get Ctxt

 432 |          meta <- get MD

 434 |          -- Search the correct name by location for more precise search

 435 |          -- and fallback to given name if nothing found

 436 |          let name = fromMaybe name

 437 |                   $ findInTree (line-1, col) name (nameLocMap meta)

 439 |          -- Lookup the name globally

 440 |          globals <- lookupCtxtName name (gamma defs)

 442 |          -- Get the Doc for the result

 443 |          globalResult <- case globals of

 444 |            [] => pure Nothing

 445 |            ts => do tys <- traverse (displayType False defs) ts

 446 |                     pure $ Just (vsep $ map (reAnnotate Pretty.Syntax) tys)

 448 |          -- Lookup the name locally (The name at the specified position)

 449 |          localResult <- findTypeAt $ anyAt $ within (line-1, col)

 451 |          case (globalResult, localResult) of

 452 |               -- Give precedence to the local name, as it shadows the others

 453 |               (_, Just (n, _, type)) => pure $ DisplayEdit $

 454 |                 prettyLocalName n <++> colon <++> !(reAnnotate Syntax <$> displayTerm defs type)

 455 |               (Just globalDoc, Nothing) => pure $ DisplayEdit $ globalDoc

 456 |               (Nothing, Nothing) => undefinedName replFC name

 458 |   where

 460 |     prettyLocalName : Name -> Doc IdrisAnn

 461 |     -- already looks good

 462 |     prettyLocalName nm@(UN _) = pretty0 nm

 463 |     prettyLocalName nm@(NS _ (UN _)) = pretty0 nm

 464 |     -- otherwise

 465 |     prettyLocalName nm = case userNameRoot nm of

 466 |       -- got rid of `Nested` or `PV`

 467 |       Just nm => pretty0 nm

 468 |       -- really bad case e.g. case block name

 469 |       Nothing => pretty0 (nameRoot nm)

 471 | processEdit (CaseSplit upd line col name)

 472 |     = do let find = if col > 0

 473 |                        then within (line-1, col-1)

 474 |                        else onLine (line-1)

 475 |          OK splits <- getSplits (anyAt find) name

 476 |              | SplitFail err => pure (EditError (pretty0 $ show err))

 477 |          lines <- updateCase splits (line-1) (col-1)

 478 |          if upd

 479 |             then updateFile (caseSplit (unlines lines) (integerToNat (cast (line - 1))))

 480 |             else pure $ DisplayEdit (vsep $ pretty0 <$> lines)

 481 | processEdit (AddClause upd line name)

 482 |     = do Just c <- getClause line name

 483 |              | Nothing => pure (EditError (pretty0 name <++> reflow "not defined here"))

 484 |          if upd

 485 |             then updateFile (addClause c (integerToNat (cast line)))

 486 |             else pure $ DisplayEdit (pretty0 c)

 487 | processEdit (Intro upd line hole)

 488 |     = do defs <- get Ctxt

 489 |          -- Grab the hole's definition (and check it is not a solved hole)

 490 |          [(h, hidx, hgdef)] <- lookupCtxtName hole (gamma defs)

 491 |            | _ => pure $ EditError ("Could not find hole named" <++> pretty0 hole)

 492 |          let Hole args _ = definition hgdef

 493 |            | _ => pure $ EditError (pretty0 hole <++> "is not a refinable hole")

 494 |          let (lhsCtxt ** (env, htyInLhsCtxt)) = underPis (cast args) Env.empty (type hgdef)

 496 |          (iintrod :: iintrods) <- intro hidx hole env htyInLhsCtxt

 497 |            | [] => pure $ EditError "Don't know what to do."

 498 |          pintrods <- traverseList1 pterm (iintrod ::: iintrods)

 499 |          syn <- get Syn

 500 |          let brack = elemBy (\x, y => dropNS x == dropNS y) hole (bracketholes syn)

 501 |          let introds = map (show . pretty . ifThenElse brack (addBracket replFC) id) pintrods

 503 |          if upd

 504 |             then case introds of

 505 |                    introd ::: [] => updateFile (proofSearch hole introd (integerToNat (cast (line - 1))))

 506 |                    _ => pure $ EditError "Don't know what to do"

 507 |             else pure $ MadeIntro introds

 508 | processEdit (Refine upd line hole e)

 509 |     = do defs <- get Ctxt

 510 |          -- First we grab the hole's definition (and check it is not a solved hole)

 511 |          -- We grab the LHS it lives in as well as its type in that context.

 512 |          [(h, hidx, hgdef)] <- lookupCtxtName hole (gamma defs)

 513 |            | _ => pure $ EditError ("Could not find hole named" <++> pretty0 hole)

 514 |          let Hole args _ = definition hgdef

 515 |            | _ => pure $ EditError (pretty0 hole <++> "is not a refinable hole")

 516 |          let (lhsCtxt ** (env, htyInLhsCtxt)) = underPis (cast args) Env.empty (type hgdef)

 518 |          -- Then we elaborate the expression we were given and infer its type.

 519 |          -- We have some magic built-in if the expression happens to be a single identifier

 520 |          -- corresponding to a top-level definition

 521 |          Right msize_tele_fun <- case e of

 522 |              PRef fc v => do

 523 |                (n :: ns) <- lookupCtxtName v (gamma defs)

 524 |                  -- could not find the variable: it may be a local one!

 525 |                  | [] => pure (Right Nothing)

 526 |                let sizes = (n ::: ns) <&> \ (_,_,gdef) =>

 527 |                               let ctxt = underPis (-1) Env.empty (type gdef) in

 528 |                               lengthExplicitPi $ fst $ snd $ ctxt

 529 |                let True = all (head sizes ==) sizes

 530 |                  | _ => pure (Left ("Ambiguous name" <++> pretty0 v <++> "(couldn't infer arity)"))

 531 |                let arity = args + head sizes -- pretending the term has been elaborated in the LHS context

 532 |                pure (Right $ Just arity)

 533 |              _ => pure (Right Nothing)

 534 |            | Left err => pure (EditError err)

 535 |          -- We do it in an extended context corresponding to the hole's so that users

 536 |          -- may mention variables bound on the LHS.

 537 |          size_tele_fun <- case msize_tele_fun of

 538 |              Just n => pure n

 539 |              Nothing => do

 540 |                ust <- get UST

 541 |                syn <- get Syn

 542 |                md <- get MD

 543 |                defs <- branch

 544 |                infered <- inferAndElab InExpr e env

 545 |                put UST ust

 546 |                put Syn syn

 547 |                put MD md

 548 |                put Ctxt defs

 549 |                let tele = underPis (-1) env $ typeOf infered

 550 |                pure (lengthExplicitPi $ fst $ snd tele)

 552 |          -- Now that we have a hole & a function to use inside it,

 553 |          -- we need to figure out how many arguments to pass to the function so that the types align

 555 |          -- E.g. refining `?hole : Nat` with the function `plus : Nat -> Nat -> Nat`

 556 |          -- means we need to replace the hole with `plus ?hole_1 ?hole_2`

 557 |          -- while refining it with the constructor `Z : Nat` means we can just return `Z`.

 559 |          -- Crude heuristics: measure the length of both *explicit* telescopes and pass

 560 |          -- |tele_fun| - |tele_hole| arguments.

 561 |          -- This may not always work because

 562 |          -- e.g.         fun   : (a : Type) -> {n : Nat} -> Vect n a

 563 |          -- won't fit in ?hole : (a : Type) -> Vect 3 a

 564 |          -- without eta-expansion to (\ a => fun a)

 565 |          -- It is hopefully a good enough approximation for now. A very ambitious approach

 566 |          -- would be to type-align the telescopes. Bonus points for allowing permutations.

 567 |          let size_tele_hole = lengthExplicitPi $ fst $ snd $ underPis (-1) Env.empty (type hgdef)

 568 |          let True = size_tele_fun >= size_tele_hole

 569 |            | _ => pure $ EditError $ hsep

 570 |                        [ "Cannot seem to refine", pretty0 hole

 571 |                        , "by", pretty0 (show e) ]

 573 |          -- We now have all the necessary information to manufacture the function call

 574 |          -- that starts with the expression the user passed

 575 |          call <- do -- We're forming the PTerm (e ?hole_1 ... ?hole_|missing_args|)

 576 |                     -- We don't reuse etm because it may have been elaborated to something dodgy

 577 |                     -- because of defaulting instances.

 578 |                     let n = minus size_tele_fun size_tele_hole

 579 |                     ns <- uniqueHoleNames defs n (nameRoot hole)

 580 |                     let new_holes = PHole replFC True <$> ns

 581 |                     let pcall = papply replFC e new_holes

 583 |                     -- We're desugaring it to the corresponding TTImp

 584 |                     icall <- desugar AnyExpr (lhsCtxt <>> []) pcall

 586 |                     -- We're checking this term full of holes against the type of the hole

 587 |                     -- TODO: branch before checking the expression fits

 588 |                     --       so that we can cleanly recover in case of error

 589 |                     let gty = gnf env htyInLhsCtxt

 590 |                     ccall <- checkTerm hidx {-is this correct?-} InExpr [] (MkNested []) env icall gty

 592 |                     -- And then we normalise, unelab, resugar the resulting term so

 593 |                     -- that solved holes are replaced with their solutions

 594 |                     -- (we need to re-read the context because elaboration may have added solutions to it)

 595 |                     defs <- get Ctxt

 596 |                     ncall <- normaliseHoles defs env ccall

 597 |                     pcall <- resugar env ncall

 598 |                     syn <- get Syn

 599 |                     let brack = elemBy (\x, y => dropNS x == dropNS y) hole (bracketholes syn)

 600 |                     pure $ show $ ifThenElse brack (addBracket replFC) id pcall

 602 |          if upd

 603 |             then updateFile (proofSearch hole call (integerToNat (cast (line - 1))))

 604 |             else pure $ DisplayEdit (pretty0 call)

 606 | processEdit (ExprSearch upd line name hints)

 607 |     = do defs <- get Ctxt

 608 |          syn <- get Syn

 609 |          let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)

 610 |          case !(lookupDefName name (gamma defs)) of

 611 |               [(n, nidx, Hole locs _)] =>

 612 |                   do let searchtm = exprSearch replFC name hints

 613 |                      update ROpts { psResult := Just (name, searchtm) }

 614 |                      Just (_, restm) <- nextProofSearch

 615 |                           | Nothing => pure $ EditError "No search results"

 616 |                      let tm' = dropLams locs restm

 617 |                      itm <- pterm $ map defaultKindedName tm' -- hack

 618 |                      let itm'  = ifThenElse brack (addBracket replFC itm) itm

 619 |                      if upd

 620 |                         then updateFile (proofSearch name (show itm') (integerToNat (cast (line - 1))))

 621 |                         else pure $ DisplayEdit (prettyBy Syntax itm')

 622 |               [(n, nidx, PMDef pi [] (STerm _ tm) _ _)] =>

 623 |                   case holeInfo pi of

 624 |                        NotHole => pure $ EditError "Not a searchable hole"

 625 |                        SolvedHole locs =>

 626 |                           do let (_ ** (env, tm')) = dropLamsTm locs Env.empty !(normaliseHoles defs Env.empty tm)

 627 |                              itm <- resugar env tm'

 628 |                              let itm'= ifThenElse brack (addBracket replFC itm) itm

 629 |                              if upd

 630 |                                 then updateFile (proofSearch name (show itm') (integerToNat (cast (line - 1))))

 631 |                                 else pure $ DisplayEdit (prettyBy Syntax itm')

 632 |               [] => pure $ EditError $ "Unknown name" <++> pretty0 name

 633 |               _ => pure $ EditError "Not a searchable hole"

 634 | processEdit ExprSearchNext

 635 |     = do defs <- get Ctxt

 636 |          syn <- get Syn

 637 |          Just (name, restm) <- nextProofSearch

 638 |               | Nothing => pure $ EditError "No more results"

 639 |          [(n, nidx, Hole locs _)] <- lookupDefName name (gamma defs)

 640 |               | _ => pure $ EditError "Not a searchable hole"

 641 |          let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)

 642 |          let tm' = dropLams locs restm

 643 |          itm <- pterm $ map defaultKindedName tm'

 644 |          let itm' = ifThenElse brack (addBracket replFC itm) itm

 645 |          pure $ DisplayEdit (prettyBy Syntax itm')

 647 | processEdit (GenerateDef upd line name rej)

 648 |     = do defs <- get Ctxt

 649 |          Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine (line - 1) p)

 650 |              | Nothing => pure (EditError ("Can't find declaration for" <++> pretty0 name

 651 |                                           <++> "on line" <++> byShow line))

 652 |          case !(lookupDefExact n' (gamma defs)) of

 653 |               Just None =>

 654 |                  do let searchdef = makeDefSort (\p, n => onLine (line - 1) p)

 655 |                                                 16 mostUsed n'

 656 |                     update ROpts { gdResult := Just (line, searchdef) }

 657 |                     Just (_, (fc, cs)) <- nextGenDef rej

 658 |                          | Nothing => pure (EditError "No search results")

 660 |                     let l : Nat = integerToNat $ cast $ startCol (toNonEmptyFC fc)

 662 |                     Just srcLine <- getSourceLine line

 663 |                        | Nothing => pure (EditError "Source line not found")

 664 |                     let (markM, srcLineUnlit) = isLitLine srcLine

 665 |                     ls <- traverse (printClause markM l) cs

 666 |                     if upd

 667 |                        then updateFile (addClause (unlines ls) (integerToNat (cast line)))

 668 |                        else pure $ DisplayEdit (vsep $ pretty0 <$> ls)

 669 |               Just _ => pure $ EditError "Already defined"

 670 |               Nothing => pure $ EditError $ "Can't find declaration for" <++> pretty0 name

 671 | processEdit GenerateDefNext

 672 |     = do Just (line, (fc, cs)) <- nextGenDef 0

 673 |               | Nothing => pure (EditError "No more results")

 674 |          let l : Nat = integerToNat $ cast $ startCol (toNonEmptyFC fc)

 675 |          Just srcLine <- getSourceLine line

 676 |             | Nothing => pure (EditError "Source line not found")

 677 |          let (markM, srcLineUnlit) = isLitLine srcLine

 678 |          ls <- traverse (printClause markM l) cs

 679 |          pure $ DisplayEdit (vsep $ pretty0 <$> ls)

 680 | processEdit (MakeLemma upd line name)

 681 |     = do defs <- get Ctxt

 682 |          syn <- get Syn

 683 |          let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)

 684 |          case !(lookupDefTyName name (gamma defs)) of

 685 |               [(n, nidx, Hole locs _, ty)] =>

 686 |                   do (lty, lapp) <- makeLemma replFC name locs ty

 687 |                      pty <- pterm $ map defaultKindedName lty -- hack

 688 |                      papp <- pterm $ map defaultKindedName lapp -- hack

 689 |                      let pappstr = show (ifThenElse brack

 690 |                                             (addBracket replFC papp)

 691 |                                             papp)

 692 |                      Just srcLine <- getSourceLine line

 693 |                        | Nothing => pure (EditError "Source line not found")

 694 |                      let (markM,_) = isLitLine srcLine

 695 |                      if upd

 696 |                         then updateFile (addMadeLemma markM name (show pty) pappstr

 697 |                                                       (max 0 (integerToNat (cast (line - 1)))))

 698 |                         else pure $ MadeLemma markM name pty pappstr

 699 |               _ => pure $ EditError "Can't make lifted definition"

 700 | processEdit (MakeCase upd line name)

 701 |     = do litStyle <- getLitStyle

 702 |          syn <- get Syn

 703 |          let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)

 704 |          Just src <- getSourceLine line

 705 |               | Nothing => pure (EditError "Source line not available")

 706 |          let Right l = unlit litStyle src

 707 |               | Left err => pure (EditError "Invalid literate Idris")

 708 |          let (markM, _) = isLitLine src

 709 |          let c = lines $ makeCase brack name l

 710 |          if upd

 711 |             then updateFile (addMadeCase markM c (max 0 (integerToNat (cast (line - 1)))))

 712 |             else pure $ MadeCase markM c

 713 | processEdit (MakeWith upd line name)

 714 |     = do litStyle <- getLitStyle

 715 |          Just src <- getSourceLine line

 716 |               | Nothing => pure (EditError "Source line not available")

 717 |          let Right l = unlit litStyle src

 718 |               | Left err => pure (EditError "Invalid literate Idris")

 719 |          let (markM, _) = isLitLine src

 720 |          let w = lines $ makeWith name l

 721 |          if upd

 722 |             then updateFile (addMadeCase markM w (max 0 (integerToNat (cast (line - 1)))))

 723 |             else pure $ MadeWith markM w

 725 | prepareExp :

 726 |     {auto c : Ref Ctxt Defs} ->

 727 |     {auto u : Ref UST UState} ->

 728 |     {auto s : Ref Syn SyntaxInfo} ->

 729 |     {auto m : Ref MD Metadata} ->

 730 |     {auto o : Ref ROpts REPLOpts} ->

 731 |     PTerm -> Core ClosedTerm

 732 | prepareExp ctm

 733 |     = do ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN $ Basic "unsafePerformIO")) ctm)

 734 |          let ttimpWithIt = ILocal replFC !getItDecls ttimp

 735 |          inidx <- resolveName (UN $ Basic "[input]")

 736 |          (tm, ty) <- elabTerm inidx InExpr [] (MkNested [])

 737 |                                  Env.empty ttimpWithIt Nothing

 738 |          tm_erased <- linearCheck replFC linear True Env.empty tm

 739 |          compileAndInlineAll

 740 |          pure tm_erased

 742 | processLocal : {vars : _} ->

 743 |              {auto c : Ref Ctxt Defs} ->

 744 |              {auto m : Ref MD Metadata} ->

 745 |              {auto u : Ref UST UState} ->

 746 |              {auto e : Ref EST (EState vars)} ->

 747 |              {auto s : Ref Syn SyntaxInfo} ->

 748 |              {auto o : Ref ROpts REPLOpts} ->

 749 |              List ElabOpt ->

 750 |              NestedNames vars -> Env Term vars ->

 751 |              List ImpDecl -> (scope : List ImpDecl) ->

 752 |              Core ()

 753 | processLocal {vars} eopts nest env nestdecls_in scope

 754 |     = localHelper nest env nestdecls_in $ \nest' => traverse_ (processDecl eopts nest' env) scope

 757 | execExp : {auto c : Ref Ctxt Defs} ->

 758 |           {auto u : Ref UST UState} ->

 759 |           {auto s : Ref Syn SyntaxInfo} ->

 760 |           {auto m : Ref MD Metadata} ->

 761 |           {auto o : Ref ROpts REPLOpts} ->

 762 |           PTerm -> Core REPLResult

 763 | execExp ctm

 764 |     = do Just cg <- findCG

 765 |            | Nothing =>

 766 |               do iputStrLn (reflow "No such code generator available")

 767 |                  pure CompilationFailed

 768 |          tm_erased <- prepareExp ctm

 769 |          logTimeWhen !getEvalTiming 0 "Execution" $

 770 |            execute cg tm_erased

 771 |          pure $ Executed ctm

 774 | execDecls : {auto c : Ref Ctxt Defs} ->

 775 |             {auto u : Ref UST UState} ->

 776 |             {auto s : Ref Syn SyntaxInfo} ->

 777 |             {auto m : Ref MD Metadata} ->

 778 |             {auto o : Ref ROpts REPLOpts} ->

 779 |             List PDecl -> Core REPLResult

 780 | execDecls decls = do

 781 |   traverse_ execDecl decls

 782 |   pure DefDeclared

 783 |   where

 784 |     execDecl : PDecl -> Core ()

 785 |     execDecl decl = do

 786 |       i <- desugarDecl [] decl

 787 |       inidx <- resolveName (UN $ Basic "[defs]")

 788 |       _ <- newRef EST (initEStateSub inidx Env.empty Refl)

 789 |       processLocal [] (MkNested []) Env.empty !getItDecls i

 792 | compileExp : {auto c : Ref Ctxt Defs} ->

 793 |              {auto u : Ref UST UState} ->

 794 |              {auto s : Ref Syn SyntaxInfo} ->

 795 |              {auto m : Ref MD Metadata} ->

 796 |              {auto o : Ref ROpts REPLOpts} ->

 797 |              PTerm -> String -> Core REPLResult

 798 | compileExp ctm outfile

 799 |     = do Just cg <- findCG

 800 |               | Nothing =>

 801 |                    do iputStrLn (reflow "No such code generator available")

 802 |                       pure CompilationFailed

 803 |          tm_erased <- prepareExp ctm

 804 |          ok <- compile cg tm_erased outfile

 805 |          maybe (pure CompilationFailed)

 806 |                (pure . Compiled)

 807 |                ok

 810 | loadMainFile : {auto c : Ref Ctxt Defs} ->

 811 |                {auto u : Ref UST UState} ->

 812 |                {auto s : Ref Syn SyntaxInfo} ->

 813 |                {auto m : Ref MD Metadata} ->

 814 |                {auto o : Ref ROpts REPLOpts} ->

 815 |                String -> Core REPLResult

 816 | loadMainFile f

 817 |     = do update ROpts { evalResultName := Nothing }

 818 |          modIdent <- ctxtPathToNS f

 819 |          resetContext (PhysicalIdrSrc modIdent)

 820 |          Right res <- coreLift (readFile f)

 821 |             | Left err => do setSource ""

 822 |                              pure (ErrorLoadingFile f err)

 823 |          errs <- logTime 1 "Build deps" $ buildDeps f

 824 |          updateErrorLine errs

 825 |          setSource res

 826 |          resetProofState

 827 |          case errs of

 828 |            [] => pure (FileLoaded f)

 829 |            _ => pure (ErrorsBuildingFile f errs)

 834 | replEval : {auto c : Ref Ctxt Defs} ->

 835 |            {vs : _} ->

 836 |            REPLEval -> Defs -> Env Term vs -> Term vs -> Core (Term vs)

 837 | replEval NormaliseAll = normaliseOpts ({ strategy := CBV } withAll)

 838 | replEval _ = normalise

 841 | inferAndNormalize : {auto c : Ref Ctxt Defs} ->

 842 |   {auto u : Ref UST UState} ->

 843 |   {auto s : Ref Syn SyntaxInfo} ->

 844 |   {auto m : Ref MD Metadata} ->

 845 |   {auto o : Ref ROpts REPLOpts} ->

 846 |   REPLEval ->

 847 |   PTerm ->

 848 |   Core (TermWithType Scope.empty)

 849 | inferAndNormalize emode itm

 850 |   = do (tm `WithType` ty) <- inferAndElab (elabMode emode) itm Env.empty

 851 |        logTerm "repl.eval" 10 "Elaborated input" tm

 852 |        defs <- get Ctxt

 853 |        let norm = replEval emode

 854 |        ntm <- norm defs Env.empty tm

 855 |        logTermNF "repl.eval" 5 "Normalised" Env.empty ntm

 856 |        pure $ ntm `WithType` ty

 857 |   where

 858 |     elabMode : REPLEval -> ElabMode

 859 |     elabMode EvalTC = InType

 860 |     elabMode _ = InExpr

 868 | process : {auto c : Ref Ctxt Defs} ->

 869 |           {auto u : Ref UST UState} ->

 870 |           {auto s : Ref Syn SyntaxInfo} ->

 871 |           {auto m : Ref MD Metadata} ->

 872 |           {auto o : Ref ROpts REPLOpts} ->

 873 |           REPLCmd -> Core REPLResult

 874 | process (NewDefn decls) = execDecls decls

 875 | process (Eval itm)

 876 |     = do opts <- get ROpts

 877 |          let emode = evalMode opts

 878 |          case emode of

 879 |             Execute => do ignore (execExp itm); pure (Executed itm)

 880 |             Scheme =>

 881 |               do (tm `WithType` ty) <- inferAndElab InExpr itm Env.empty

 882 |                  qtm <- logTimeWhen !getEvalTiming 0 "Evaluation" $

 883 |                            (do nf <- snfAll Env.empty tm

 884 |                                quote Env.empty nf)

 885 |                  itm <- logTimeWhen False 0 "Resugar" $ resugar Env.empty qtm

 886 |                  pure (Evaluated itm Nothing)

 887 |             _ =>

 888 |               do (ntm `WithType` ty) <- logTimeWhen !getEvalTiming 0 "Evaluation" $

 889 |                                            inferAndNormalize emode itm

 890 |                  itm <- resugar Env.empty ntm

 891 |                  defs <- get Ctxt

 892 |                  opts <- get ROpts

 893 |                  let norm = replEval emode

 894 |                  evalResultName <- DN "it" <$> genName "evalResult"

 895 |                  ignore $ addDef evalResultName

 896 |                    $ newDef replFC evalResultName top Scope.empty ty defaulted

 897 |                    $ PMDef defaultPI Scope.empty (STerm 0 ntm) (STerm 0 ntm) []

 898 |                  addToSave evalResultName

 899 |                  put ROpts ({ evalResultName := Just evalResultName } opts)

 900 |                  if showTypes opts

 901 |                     then do ity <- resugar Env.empty !(norm defs Env.empty ty)

 902 |                             pure (Evaluated itm (Just ity))

 903 |                     else pure (Evaluated itm Nothing)

 904 | process (Check (PRef fc (UN (Basic "it"))))

 905 |     = do opts <- get ROpts

 906 |          case evalResultName opts of

 907 |               Nothing => throw (UndefinedName fc (UN $ Basic "it"))

 908 |               Just n => process (Check (PRef fc n))

 909 | process (Check (PRef fc fn))

 910 |     = do defs <- get Ctxt

 911 |          case !(lookupCtxtName fn (gamma defs)) of

 912 |               [] => undefinedName fc fn

 913 |               ts => do tys <- traverse (displayType False defs) ts

 914 |                        pure (Printed $ vsep $ map (reAnnotate Syntax) tys)

 915 | process (Check itm)

 916 |     = do (tm `WithType` ty) <- inferAndElab InExpr itm Env.empty

 917 |          defs <- get Ctxt

 918 |          itm <- resugar Env.empty !(normaliseHoles defs Env.empty tm)

 919 |          -- ty <- getTerm gty

 920 |          ity <- resugar Env.empty !(normalise defs Env.empty ty)

 921 |          pure (TermChecked itm ity)

 922 | process (CheckWithImplicits itm)

 923 |     = do showImplicits <- showImplicits <$> getPPrint

 924 |          setOpt (ShowImplicits True)

 925 |          result <- process (Check itm)

 926 |          setOpt (ShowImplicits showImplicits)

 927 |          pure result

 928 | process (PrintDef (PRef fc fn))

 929 |     = do defs <- get Ctxt

 930 |          case !(lookupCtxtName fn (gamma defs)) of

 931 |               [] => undefinedName fc fn

 932 |               ts => do defs <- traverse (displayPats False defs) ts

 933 |                        pure (Printed $ vsep $ map (reAnnotate Syntax) defs)

 934 | process (PrintDef t)

 935 |     = case !(getDocsForImplementation t) of

 936 |         Just d => pure (Printed $ reAnnotate Syntax d)

 937 |         Nothing => pure (Printed $ pretty0 "Error: could not find definition of \{show t}")

 938 | process Reload

 939 |     = do opts <- get ROpts

 940 |          case mainfile opts of

 941 |               Nothing => pure NoFileLoaded

 942 |               Just f => loadMainFile f

 943 | process (Load f)

 944 |     = do update ROpts { mainfile := Just f }

 945 |          -- Clear the context and load again

 946 |          loadMainFile f

 947 | process (ImportMod m)

 948 |     = do catch (do addImport (MkImport emptyFC False m (miAsNamespace m))

 949 |                    pure $ ModuleLoaded (show m))

 950 |                (\err => pure $ ErrorLoadingModule (show m) err)

 951 | process (CD dir)

 952 |     = do setWorkingDir dir

 953 |          workDir <- getWorkingDir

 954 |          pure (CurrentDirectory workDir)

 955 | process CWD

 956 |     = do workDir <- getWorkingDir

 957 |          pure (CurrentDirectory workDir)

 958 | process Edit

 959 |     = do opts <- get ROpts

 960 |          case mainfile opts of

 961 |               Nothing => pure NoFileLoaded

 962 |               Just f =>