search

UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 23 forks source link

`point not declared in context` revisited #546

Closed ComFreek closed 3 years ago

ComFreek commented 3 years ago

Simplifying d- A B (with d- from MitM/core) throws a GeneralError with cause variable point not declared in context.

How to reproduce

  1. Get the FrameIT/frameworld archive or (simpler:) just copy the following code to somwhere accessible:
namespace http://mathhub.info/FrameIT/frameworld/integrationtests ❚

theory TheoryParameterBug : ur:?LF =
    include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
    include ☞http://mathhub.info/MitM/core/geometry?Planes ❙

    A = ⟨0.0, 0.0, 0.0⟩ ❙
    B = ⟨3.0, 3.0, 0.0⟩ ❙

    /T simplifying this constant fails: ❙
    dist = d- A B ❙
❚
  1. Run https://github.com/UniFormal/MMT/blob/devel/src/test/TheoryParameterBug.scala#L9-L19

Debugging Attempts

See our FrameIT Mattermost channel. point is accessed as a variable within the context and not as a symbol at some point.

florian-rabe commented 3 years ago

I fixed two very subtle low-level bugs on devel-names. I think that'll do it.

Generally, the treatment of parametric theories has never been thoroughly specified or tested. We fix it as we go along, and this was one such instance.

ComFreek commented 3 years ago

Thank you very much for fixing. I confirmed it to work in FrameIT now.