Incorrect hole naming

[uncomputable]

The hole in this program is named disc1 instead of hole. The following code runs:

let s = "
    id1 := iden : 2^256 * 1 -> 2^256 * 1
    disc1 := unit
    main := comp (disconnect id1 ?hole) unit -- fixme: ?hole is named disc1
";
let empty_witness = HashMap::new();
let forest = Forest::parse(s).unwrap();
let program = forest.to_witness_node(&empty_witness).finalize().unwrap();

Replacing disc1 with hole makes the code fail.

[apoelstra]

Why should it be named hole? Because there is already an expression named disc1?

[uncomputable]

There is a DAG root main with a hole ?hole and there is a DAG root hole. My goal was to write code that completes the DAG main by filling in ?hole with the DAG hole.

I think I made a mistake in the implementation.

[apoelstra]

The code you posted does not have a DAG root named hole.

[apoelstra]

Since you are fixing this issue, can you describe it in a way that I understand?

[uncomputable]

There was a misunderstanding in the above messages. The issue is about the following:

Take the following program. There is a hole called hole.

id1 := iden : 2^256 * 1 -> 2^256 * 1
main := comp (disconnect id1 ?hole) unit

We have the concept of roots that form a forest. The main root is special because it defines the program itself. Other roots define expressions which can be used to fill holes.

I define a root called hole.

hole := unit

The current human encoding code is unable to match the hole called hole with the root called hole. In fact, the name of the hole is disregarded and a generic name is assigned. (In the example of the topmost message, this name is disc1).

The correct behavior would be to keep the hole name hole and to match it with the root name hole.

The unit test filled hole tests this behavior.

[apoelstra]

The correct behavior would be to keep the hole name hole and to match it with the root name hole.

Hmmmmm, interesting. I guess that is useful behavior, though it's a little dangerous because it may give the impression that the user is able to fill holes at commitment time. I think we may want to output a warning if you try to fill a hole with an expression from the same file / same forest like this.

But in general yes, I agree it's a bug that we're completely losing the name and not able to match that up with the hole. We do want users to be able to name holes and provide expressions to fill them.