search

idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.53k stars 378 forks source link

Add new commands to repl `:show import` (to show already imported modules) and `:show loaded` (all available) #3410

Open srghma opened 3 weeks ago

srghma commented 3 weeks ago

Motivation

will be used in https://github.com/idris-community/idris2-lsp/issues/227

Examples

so, if I have dependencies = base, filepath in ipkg, then :show loaded will show Data.Vect and Data.FilePath and Data.FilePath.File, etc.

just like in purescript

2024-11-02-02pm-48-12-screenshot

Technical implementation

Alternatives considered

maybe better

  1. show imported_modules - modules in scope, e.g. import Data.Vect (same as show import from purescript)
  2. show loaded_modules - all available modules from all available packages ( same as show loaded from purescript)
  3. show imported_packages - IF before I did :package "filepath" THEN will show filepath - imported completely ELSEIF before I did import Data.Vect THEN will show base - imported partially
  4. show loaded_packages - if dependencies = base, filepath then will show base, filepath

Conclusion