Search code examples
development-environmentmmt

Finding out in which MMT source file a constant/theory/... was declared

Say I remember a constant or theory name, but totally forgot where it is declared. Perhaps, I don't even know in which MMT archive it is declared. How can I find out the source file?

Can I just open an MMT shell, load all archives I have on my disk, and issue some command find_constant <constant name>? Does such a command exist?

Solution

  • It depends on what you know about the thing whose declaration point you seek:

    • If you don't know anything, i.e. if you don't even have a typechecking file where the thing is used.

      Then the easiest way to find out the point of declaration is to just grep over all *.mmt files with regexes. For (typed) constants, use <constant name>\s*?:. It will match constant declarations, followed by some optional whitespace, and a colon.

      With Notepad++, this is easy to do. Say, you wanted to know where congT is declared. Then you would do:

      enter image description here

    • You have a typechecking MMT file where the thing you are looking for is used.

      Then use the MMT IntelliJ plugin and its document tree: first typecheck the file at hand, and then look in the sidekick for the occurrence of the constant:

      enter image description here

      Activating the Navigate option is particularly helpful here: with that you can simply click with your mouse on the thing whose point of declaration you seek (here e.g. nat_lit) and immediately have it revealed in the sidekick. Here, the sidekick shows nat_lit (?NatLiterals) meaning that the constant was defined in the theory NatLiterals. Ideally, you know where that theory is declared.

      In theory, you could also control-click on the constant, but that doesn't currently work for reasons beyond my knowledge.