Deducteam
Goto definition ignores qualifier
In file tests/OK/PrintB.lp
symbol f:B→B→B
compute a+a // should print a+a
compute tests.OK.PrintA.f a a // should print a+a
^
Goto definition goes to the f defined in PrintB rather than PrintA
Can't test right now due to some other brokeness, what does the symbol map contain tho?
Hello @ejgallego , contents of symbol map:
569 [do_definition]: No symbol found
570 [symbol map]: {#cons} / #cons: unknown location
571 {#equiv} / #equiv: unknown location
572 {+} / g: file:///home/ashish/lambdapi/tests/OK/PrintB.lp, 0:0-20
573 {;} / #cons: unknown location
574 {A} / A: /home/ashish/lambdapi/tests/OK/PrintA.lp, 1:7-8
575 {B} / B: file:///home/ashish/lambdapi/tests/OK/PrintB.lp, 0:7-8
576 {a} / a: /home/ashish/lambdapi/tests/OK/PrintA.lp, 2:7-8
577 {b} / b: file:///home/ashish/lambdapi/tests/OK/PrintB.lp, 0:7-8
578 {f} / f: file:///home/ashish/lambdapi/tests/OK/PrintB.lp, 0:7-8
579 {g} / g: file:///home/ashish/lambdapi/tests/OK/PrintB.lp, 0:7-8
580 {×} / f: file:///home/ashish/lambdapi/tests/OK/PrintB.lp, 0:0-20
I see now, thanks; so there are two problems I speculate:
- one due to the map not having proper qualification, the local symbol overwrittes the one in
PrintA - tokenization seems to be too low-level, we should work at the qid level to get the fully qualified name.
In general it seems to me that the whole code doing the position -> sentence inverse map needs general improvements.
The problem is that the rangemap is built from the AST where non-qualified identifiers have not been resolved yet as it depends on which modules are open and in which order they are open. We already encountered a similar problem in Pratt parsing. This means that we should probably split scoping in two phases: one that resolves identifiers, and one that transforms p_term's into term's. To do this, I suggest to add in p_term new constructors P_symb and P_vari. Perhaps, in a second step, we could even remove P_iden and scope identifiers during lexing (as commands are parsed one by one now) by passing to the lexer the function Sig_state.find_sym that resolves identifiers.
