bugfix: make view Float.mod.doc not crash

[mitchellwrosen]

Overview

Fixes #5520

This is a weird one. view Float.mod.doc caused UCM to crash, ultimately because we were calling Name.splits on an absolute name, which you aren't supposed to do.

The fix implemented here is to simply not call Name.splits on absolute names. This seems fine, because we are only calling Name.splits on names in order to count their uses, for the purpose of possibly inserting a use clause to clean some stuff up. So, a consequence of this particular fix is we won't ever (say) shorten something like

.foo.bar + .foo.bar + .foo.bar

to

use .foo bar
bar + bar + bar

Given how incredibly fragile this particular part of term parsing and printing is, with respect to variable capture, I think that's an ok compromise.

On to the root cause: I think there is an issue in the doc parser. Take a look at a rendering of part of Float.mod.doc:

Notice that Float.- is a clickable thing, but none of Float.floor, Float./, or Float.* are. Why is that?

Simplifying the example a bit,

{{ ``x Float.* floor y`` }}

this comes out of the doc parser as

Paragraph
  [ Special 
      (  Example
          3 
          ( Term.Term 
              ( Any (do x Float.floor y -> x Float.* Float.floor y) )
          )
      )
  ]

Note that Float.* is free, but Float.floor is bound for some reason (which is especially curious since I originally wrote the expression as floor and let TDNR resolve it to Float.floor). That ultimately explains why the "avoid shadowing" logic in our term printer kicks in and has to render some Float.* with a leading dot, due to the (overly-conservative) logic that only cares whether a variable is bound anywhere in a term.

Test coverage

I've only tested this manually, but could add a transcript that tries to distill down the problem and solution. I'm hesitant to do that, though, because I suspect a fix to the doc parser would essentially make that transcript not really test anything important. So, it's plausible (to me) that a manual test is fine for this one.