format-args returns strings that introduce strange behavior (#numbers behind atoms and (parse $string) not working)

[zariuq]

Describe the bug
The format-args function seems to represent strings in a weird way that messes up behavior when evaluating the output as a string. For example, parse fails to evaluate it.

Further, when called in a function, a strange hash # is appended, whereas (parse (repr $x)) return the identity as one would expect.

To Reproduce

MeTTa HE 0.2.6 via Docker. REPL.

Expected behavior
What I expected to happen: simply adding a $ before an atom to create a variable.

> !(let $x (format-args ${} (⟨t⟩)) (parse $x))
[$⟨t⟩]

> !(parse (format-args {} (⟨t⟩)))
[⟨t⟩]

> !(parse "$⟨t⟩")
[$⟨t⟩]

> !(let $x (format-args ${} (⟨t⟩)) (repr $x))
["\"$⟨t⟩\""] ;; the same as !(let $x (repr ⟨t⟩) (repr $x))

> !(let $x (format-args ${} (⟨t⟩)) (parse (repr $x)))
["$⟨t⟩"] ;; the same as !(let $x (repr ⟨t⟩) (parse (repr $x)))

> !(let $x (format-args ${} (⟨t⟩)) (parse (parse (repr $x))))
[$⟨t⟩]

> (= (make_var $x) (let $v (format-args ${} ($x)) (parse (parse (repr $v)))))
> !(make_var ⟨t⟩)
[$⟨t⟩]

> (= (make_var $x) (let $v (format-args ${} ($x)) $v))
> !(make_var ⟨t⟩)
["$⟨t⟩"]

> (= (make_var $x) (parse (repr $x)))
> !(make_var ⟨t⟩)
[⟨t⟩]

Actual behavior
What actually happened:

> !(let $x (format-args ${} (⟨t⟩)) (parse $x))
[(parse "$⟨t⟩")]

> !(parse (format-args {} (⟨t⟩)))
[(parse "⟨t⟩")]

> !(parse "$⟨t⟩")
[$⟨t⟩]

These let versions behaves as expected.

> !(let $x (format-args ${} (⟨t⟩)) (repr $x))
["\"$⟨t⟩\""]

> !(let $x (format-args ${} (⟨t⟩)) (parse (repr $x)))
["$⟨t⟩"]

> !(let $x (format-args ${} (⟨t⟩)) (parse (parse (repr $x))))
[$⟨t⟩]

Now they behave weridly with the #s.

> (= (make_var $x) (let $v (format-args ${} ($x)) (parse (parse (repr $v)))))
> !(make_var ⟨t⟩)
[(parse "$⟨t⟩#1429682")]

> (= (make_var $x) (let $v (format-args ${} ($x)) $v))
> !(make_var ⟨t⟩)
["$⟨t⟩#1430218"]

> (= (make_var $x) (parse (repr $x)))
> !(make_var ⟨t⟩)
[⟨t⟩]

[vsbogd]

> !(let $x (format-args ${} (⟨t⟩)) (parse $x))
[(parse "$⟨t⟩")]

> !(parse (format-args {} (⟨t⟩)))
[(parse "⟨t⟩")]

> !(parse "$⟨t⟩")
[$⟨t⟩]

Code above is actually a not-finished work on implicit type conversion. Raised #979 to fix it.

[vsbogd]

> (= (make_var $x) (let $v (format-args ${} ($x)) $v))
> !(make_var ⟨t⟩)
["$⟨t⟩#1430218"]

I don't have clear explanation to result, but if you add quotes around "${}" (as actually expected) it will work. The unexpected result is returned because ${} is actually a variable not a pattern.

> (= (make_var $x) (let $v (format-args ${} ($x)) (parse (parse (repr $v)))))
> !(make_var ⟨t⟩)
[(parse "$⟨t⟩#1429682")]

The same as above, using quotes will fix this. But in fact I don't understand why you are expecting a variable returned. I would expect (parse $<t>) is returned because parse should not work on variable as an argument (try !(parse $<t>)).

[zariuq]

Ah, great, I often don't know if I'm just being ignorant of something basic (re the quotes) or there's some bug (or both).

This may work for the workaround. Thank you!

> (= (make_var1 $x) (let $v (format-args "${}" ($x)) (parse (parse (repr $v)))))
> !(make_var1 ⟨t⟩)
[$⟨t⟩]

The repr adds a layer of quotes around the string (so we have "s), then parse strips the first layer, and the next parse strips the second. Which leaves one with a variable atom, I think?

I'm not sure this is the best way to do what I'm after. I have a mathetacial expression with some symbols that I'd like to turn into variables, and this was one approach that I thought might work. I'm going from an object language to MeTTa, and in the object language, the "variables" are represented as symbol atoms to avoid being treated as MeTTa variables.

[vsbogd]

I often don't know if I'm just being ignorant of something basic (re the quotes) or there's some bug (or both).

I will add a type check for this specific case.

The repr adds a layer of quotes around the string (so we have "s), then parse strips the first layer, and the next parse strips the second. Which leaves one with a variable atom, I think?

Ah, ok, makes sense.

I have a mathetacial expression with some symbols that I'd like to turn into variables, and this was one approach that I thought might work. I'm going from an object language to MeTTa, and in the object language, the "variables" are represented as symbol atoms to avoid being treated as MeTTa variables.

If it is about conversion symbol to variable I believe it should work. Some simplistic example would be helpful to understand if there is another solution.

[zariuq]

Some simplistic example would be helpful to understand if there is another solution.

It might be non-trivial. I guess part of the issue is the lack of global variables, so if passing around a var named $x, it should be given a different hash to distinguish it from another $x. Thus if I wish to substitute all x's in an expression for $x, I need to do it all at once, right?

I have something like the following:
((⟨wff⟩ ⟨P⟩) (⟨wff⟩ ⟨Q⟩)) ((⟨|-⟩ ⟨P⟩) (⟨|-⟩ ⟨⟦⟩ ⟨P⟩ ⟨->⟩ ⟨Q⟩ ⟨⟧⟩)) (⟨|-⟩ ⟨Q⟩))

It's broken up into multiple parts: (⟨wff⟩ ⟨P⟩) (⟨wff⟩ ⟨Q⟩), (⟨|-⟩ ⟨P⟩) (⟨|-⟩ ⟨⟦⟩ ⟨P⟩ ⟨->⟩ ⟨Q⟩ ⟨⟧⟩), and (⟨|-⟩ ⟨Q⟩)).

Mathematical term construction via the backward chainer seems to work when I tranlate the Ps and Qs into variables (-- ok, I only tested a simpler case so far). So the question is the easiest way to check which tokens are variables and to turn them into variables in a coherent manner.

For now, I'll try to find a way to just effect all the substitutions at once.

[vsbogd]

if passing around a var named $x, it should be given a different hash to distinguish it from another $x

Variable scope is a MeTTa expression. Thus $x inside an expression added into a space and $x inside an expression which is evaluated by the interpreter are different variables.

There is a requirement to keep variable names consistent for showing them to the user. Literally this works as the following. For the evaluated expressions variables are kept as is. For expression queried from space each variable is replaced by the unique instance. The unique instance is produced by adding a constantly incrementing id to the name (variable instance is a pair of the name and id), for instance $x#123. We can consider $x is always $x#-1.

(= (foo $x) $x) ; $x is replaced by $x#<n> when it is a result of the query
!(let $x 1 (foo $x)) ; $x is original variable

When (foo $x) is called the interpreter unifies (= (foo $x#<n>) ...) and (foo $x) and founds $x and $x#<n> are equal and thus logically they now are the same variable. When one of this variables is shown to the user it should always be printed as $x because this is the name which user knows.

Thus <n> are used to make variables unique and keep them inside the proper scope.

Thus if I wish to substitute all x's in an expression for $x, I need to do it all at once, right?

(parse $x) generates the $x variable without unique id like in evaluated expression. Thus if you generate it then it is considered the same $x you could use in an evaluated expression and it is always different from $x used in expression queried from space. For example the following code works:

(= (make_var $x) (let $v (format-args "${}" ($x)) (parse $v))) ; here local $x is actually $x#123 and parse produces $x so they are different

!(let $x B (A (make_var x))) ; here $x and result of make_var are equal, thus the result is [(A B)]

You can do it few times if needed:

!(let $x B (A (make_var x) (make_var x))) ; returns (A B B)
!(let A (make_var x) (let B (make_var x) (make_var x))) ; returns [] because A doesn't unify with B

[vsbogd]

You can use make_var to get global variables:

(= (foo) (make_var x))

!(let $x B (foo)) ; returns [B]

But it is not possible assign values inside of functions because interpreter cleans up values for variables which are not in outer context of the call:

(= (bar) (let (make_var y) A ()))

!(let () (bar) $y) ; returns []