0 | module Idris.REPL.Common

  2 | import Core.Directory

  3 | import Core.Env

  4 | import Core.InitPrimitives

  5 | import Core.Metadata

  6 | import Core.Unify

  8 | import Idris.Doc.Annotations

  9 | import Idris.Doc.String

 11 | import Idris.Error

 12 | import Idris.IDEMode.Commands

 13 | import Idris.IDEMode.Pretty

 14 | import Idris.Pretty

 15 | import public Idris.REPL.Opts

 16 | import Idris.Resugar

 17 | import Idris.Syntax

 18 | import Idris.Version

 20 | import Libraries.Data.ANameMap

 22 | import Data.String

 23 | import System.File

 25 | %default covering

 32 | iputStrLn : {auto c : Ref Ctxt Defs} ->

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

 34 |             Doc IdrisAnn -> Core ()

 35 | iputStrLn msg

 36 |     = do opts <- get ROpts

 37 |          case idemode opts of

 38 |               REPL InfoLvl  => coreLift $ putStrLn !(render msg)

 39 |               -- output silenced

 40 |               REPL _ => pure ()

 41 |               IDEMode i _ f =>

 42 |                 send f (WriteString

 43 |                           !(renderWithoutColor msg)

 44 |                           i)

 47 | public export

 48 | data MsgStatus = MsgStatusNone | MsgStatusError | MsgStatusInfo

 50 | doPrint : MsgStatus -> VerbosityLvl -> Bool

 51 | doPrint MsgStatusNone  InfoLvl  = True

 52 | doPrint MsgStatusNone  ErrorLvl = True

 53 | doPrint MsgStatusNone  NoneLvl  = True

 54 | doPrint MsgStatusError InfoLvl  = True

 55 | doPrint MsgStatusError ErrorLvl = True

 56 | doPrint MsgStatusError NoneLvl  = False

 57 | doPrint MsgStatusInfo  InfoLvl  = True

 58 | doPrint MsgStatusInfo  ErrorLvl = False

 59 | doPrint MsgStatusInfo  NoneLvl  = False

 61 | printWithStatus : {auto o : Ref ROpts REPLOpts} ->

 62 |                   (Doc ann -> Core String) ->

 63 |                   (Doc ann -> MsgStatus -> Core ())

 64 | printWithStatus render msg status

 65 |   = do opts <- get ROpts

 66 |        case idemode opts of

 67 |          REPL verbosityLvl =>

 68 |            case doPrint status verbosityLvl of

 69 |              True   => coreLift $ putStrLn !(render msg)

 70 |              False  => pure ()

 71 |          IDEMode {} => pure () -- this function should never be called in IDE Mode

 75 | printResult : {auto o : Ref ROpts REPLOpts} ->

 76 |               Doc IdrisAnn -> Core ()

 77 | printResult x = printWithStatus render x MsgStatusNone

 78 |  --                                      ^^^^^^^^^^^^^

 79 |  -- "results" are printed no matter the verbosity level

 83 | printDocResult : {auto o : Ref ROpts REPLOpts} ->

 84 |                  Doc IdrisDocAnn -> Core ()

 85 | printDocResult x = printWithStatus (render styleAnn) x MsgStatusNone

 86 |  --                                                    ^^^^^^^^^^^^^

 87 |  -- "results" are printed no matter the verbosity level

 91 | printError : {auto o : Ref ROpts REPLOpts} ->

 92 |              Doc IdrisAnn -> Core ()

 93 | printError msg = printWithStatus render msg MsgStatusError

 95 | DocCreator : Type -> Type

 96 | DocCreator a = a -> Core (Doc IdrisAnn)

 99 | emitProblem : {auto c : Ref Ctxt Defs} ->

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

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

102 |             a -> (DocCreator a) -> (DocCreator a) -> (a -> Maybe FC) -> MsgStatus -> Core ()

103 | emitProblem a replDocCreator idemodeDocCreator getFC status

104 |     = do opts <- get ROpts

105 |          case idemode opts of

106 |               REPL _ =>

107 |                   do msg <- replDocCreator a

108 |                      printWithStatus render msg status

109 |               IDEMode i _ f =>

110 |                   do msg <- idemodeDocCreator a

111 |                      -- TODO: Display a better message when the error doesn't contain a location

112 |                      case map toNonEmptyFC (getFC a) of

113 |                           Nothing => iputStrLn msg

114 |                           Just nfc@(origin, startPos, endPos) => do

115 |                             fname <- case origin of

116 |                               PhysicalIdrSrc ident => do

117 |                                 -- recover the file name relative to the working directory.

118 |                                 -- (This is what idris2-mode expects)

119 |                                 let fc = MkFC (PhysicalIdrSrc ident) startPos endPos

120 |                                 catch (nsToSource fc ident) (const $ pure "(File-Not-Found)")

121 |                               PhysicalPkgSrc fname =>

122 |                                 pure fname

123 |                               Virtual Interactive =>

124 |                                 pure "(Interactive)"

125 |                             let (str,spans) = !(renderWithDecorations annToProperties msg)

126 |                             send f (Warning (cast (the String fname, nfc)) str spans

127 |                                             i)

131 | emitError : {auto c : Ref Ctxt Defs} ->

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

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

134 |             Error -> Core ()

135 | emitError e = emitProblem e display perror getErrorLoc MsgStatusError

138 | emitWarning : {auto c : Ref Ctxt Defs} ->

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

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

141 |               Warning -> Core ()

142 | emitWarning w = emitProblem w displayWarning pwarning (Just . getWarningLoc) MsgStatusInfo

145 | emitWarnings : {auto c : Ref Ctxt Defs} ->

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

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

148 |                Core (List Error)

150 |     = do defs <- get Ctxt

151 |          let ws = reverse (warnings defs)

152 |          session <- getSession

153 |          if (session.warningsAsErrors)

154 |            then let errs = WarningAsError <$> ws in

155 |                 errs <$ traverse_ emitError errs

156 |            else [] <$ traverse_ emitWarning ws

159 | emitWarningsAndErrors : {auto c : Ref Ctxt Defs} ->

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

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

162 |                         List Error -> Core (List Error)

163 | emitWarningsAndErrors errs = do

164 |   ws <- emitWarnings

165 |   traverse_ emitError errs

166 |   pure ws

168 | getFCLine : FC -> Maybe Int

169 | getFCLine = map startLine . isNonEmptyFC

172 | updateErrorLine : {auto o : Ref ROpts REPLOpts} -> List Error -> Core ()

173 | updateErrorLine []       = update ROpts { errorLine := Nothing }

174 | updateErrorLine (e :: _) = update ROpts { errorLine := getErrorLoc e >>= getFCLine }

177 | resetContext : {auto c : Ref Ctxt Defs} ->

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

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

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

181 |                (origin : OriginDesc) ->

182 |                Core ()

183 | resetContext origin

184 |     = do defs <- get Ctxt

185 |          put Ctxt ({ options := clearNames (options defs) } !initDefs)

186 |          addPrimitives

187 |          put UST initUState

188 |          put Syn initSyntax

189 |          put MD (initMetadata origin)

191 | public export

192 | data EditResult : Type where

193 |   DisplayEdit : Doc IdrisAnn -> EditResult

194 |   EditError : Doc IdrisAnn -> EditResult

195 |   MadeLemma : Maybe String -> Name -> IPTerm -> String -> EditResult

196 |   MadeWith : Maybe String -> List String -> EditResult

197 |   MadeCase : Maybe String -> List String -> EditResult

198 |   MadeIntro : List1 String -> EditResult

200 | public export

201 | data MissedResult : Type where

202 |   CasesMissing : Name -> List String  -> MissedResult

203 |   CallsNonCovering : Name -> List Name -> MissedResult

204 |   AllCasesCovered : Name -> MissedResult

206 | public export

207 | data REPLResult : Type where

208 |   Done : REPLResult

209 |   REPLError : Doc IdrisAnn -> REPLResult

210 |   Executed : PTerm -> REPLResult

211 |   RequestedHelp : REPLResult

212 |   RequestedDetails : String -> REPLResult

213 |   Evaluated : IPTerm -> Maybe IPTerm -> REPLResult

214 |   Printed : Doc IdrisAnn -> REPLResult

215 |   PrintedDoc : Doc IdrisDocAnn -> REPLResult

216 |   TermChecked : IPTerm -> IPTerm -> REPLResult

217 |   FileLoaded : String -> REPLResult

218 |   ModuleLoaded : String -> REPLResult

219 |   ErrorLoadingModule : String -> Error -> REPLResult

220 |   ErrorLoadingFile : String -> FileError -> REPLResult

221 |   ErrorsBuildingFile : String -> List Error -> REPLResult

222 |   NoFileLoaded : REPLResult

223 |   CurrentDirectory : String -> REPLResult

224 |   CompilationFailed: REPLResult

225 |   Compiled : String -> REPLResult

226 |   ProofFound : IPTerm -> REPLResult

227 |   Missed : List MissedResult -> REPLResult

228 |   CheckedTotal : List (Name, Totality) -> REPLResult

229 |   OptionsSet : List REPLOpt -> REPLResult

230 |   LogLevelSet : Maybe LogLevel -> REPLResult

231 |   ConsoleWidthSet : Maybe Nat -> REPLResult

232 |   ColorSet : Bool -> REPLResult

233 |   VersionIs : Version -> REPLResult

234 |   DefDeclared : REPLResult

235 |   Exited : REPLResult

236 |   Edited : EditResult -> REPLResult

239 | docsOrSignature : {auto o : Ref ROpts REPLOpts} ->

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

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

242 |                   FC -> Name -> Core (Doc IdrisDocAnn)

243 | docsOrSignature fc n

244 |     = do syn  <- get Syn

245 |          defs <- get Ctxt

246 |          all@(_ :: _) <- lookupCtxtName n (gamma defs)

247 |              | _ => undefinedName fc n

248 |          let ns@(_ :: _) = concatMap (\n => lookupName n (defDocstrings syn))

249 |                                      (map fst all)

250 |              | [] => typeSummary defs

251 |          getDocsForName fc n MkConfig

252 |   where

253 |     typeSummary : Defs -> Core (Doc IdrisDocAnn)

254 |     typeSummary defs = do Just def <- lookupCtxtExact n (gamma defs)

255 |                             | Nothing => pure ""

256 |                           ty <- resugar Env.empty !(normaliseHoles defs Env.empty (type def))

257 |                           pure $ pretty0 n <++> ":" <++> prettyBy Syntax ty

260 | equivTypes : {auto c : Ref Ctxt Defs} ->

261 |              (ty1 : ClosedTerm) ->

262 |              (ty2 : ClosedTerm) ->

263 |              Core Bool

264 | equivTypes ty1 ty2 =

265 |   do let False = isErased ty1

266 |           | _ => pure False

267 |      logTerm "typesearch.equiv" 10 "Candidate: " ty1

268 |      defs <- get Ctxt

269 |      True <- pure (!(getArity defs Env.empty ty1) == !(getArity defs Env.empty ty2))

270 |        | False => pure False

271 |      _ <- newRef UST initUState

272 |      b <- catch

273 |            (do res <- unify inTerm EmptyFC Env.empty ty1 ty2

274 |                case res of

275 |                  (MkUnifyResult [] _ [] NoLazy) => pure True

276 |                  _ => pure False)

277 |            (\err => pure False)

278 |      when b $ logTerm "typesearch.equiv" 20 "Accepted: " ty1

279 |      pure b