Wrong formula behavior

[wweic]

drio # formula x
drio # x := 1 > 1
drio # x

I think it should return false.

[JichaoS]

Do you mean that writing x should return false? Or does x.eval() return false?

[wweic]

Oh. x.eval() do return false. But x will return an error says can not find variable.

In my experience, REPL will always evaluate the expression that we enter, so I suppose x should be equal to x.eval().

In current code, we only have two scope env, one for real vars, one for int vars. I think we also need to have an env for formula?

[scungao]

Glad you are working on this Wei.

Right now I think it's okay to separate x and x.eval(). A logic formula has a syntactic form and a semantic value. 1>1 and 2>2 have the same truth value but are still different logic formulas. Since we'll handle pretty complicated formulas, it's reasonable to delay the eval() even though it's easy to do on simple formulas.

Yes an env for formula can be useful.

[wweic]

I see. I suggest add an env for formula too. While this env only keep the raw format of formula. Only we explicitly call eval then it's evaluated.

Seems like Jichao has an env already, I'll call look up that code.

[JichaoS]

There is already an env for formula, it just stores the expr-tree that is generated when REPL reads the formula. I can also make it store the actual formula string if that could be useful later.