Concrete Values

[zaneenders]

This PR surfaces the "true error" of an expression for the local error tree in Odyessy.

Before merging:

• Finish the Unit test with correct values.
• Approx Nodes
• Display values with value->json?
• Is ulp-error correct?
• Split out true error from core and remove flag?

[pavpanchekha]

Isn't true error also possible here? Like, shouldn't it be the same as the true error in ift and iff?

[pavpanchekha]

I think this can also have true error? The exact value is the exact value of aprx-spec, the computed value is the value of impl, they can differ.

[pavpanchekha]

If this is UI-only maybe it's fine but this way of doing it is slow, because you're compiling a separate machine for every single subexpression and every single input. It would be more efficient to do this in two passes: first compute the exact value for each subexpression for each input; then compile a second machine with one input and output per subexpression and feed in each input + each subexpression's exact value for that input.

[zaneenders]

Ok i'm a little confused on this. Do you mean something like?

(define exact-var-name '__exact)
(define extended
  (for/list ([ctx (in-list ctx-list)])
    (context-extend ctx exact-var-name (context-repr ctx))))
(define compare-specs
  (for/list ([spec (in-list spec-list)])
    `(- ,spec ,exact-var-name)))
(define compare-fn (eval-progs-real compare-specs extended))