[Toss-devel] New Speagram: terms with sharing

[Lukasz S. <luk...@gm...>]

Hi,

I propose that shared subterms have two representations: either as a
sharing variable, possibly referring to a term in an accompanying
iterated substitution but it could also be a free variable, or as a
new variant, [Ref of string * term], with an implementation invariant:
two Refs in a term that have the same name contain physically equal
term. Basically, applying an iterated substitution "subst" would
replace "SVar (v, ...)" with "Rev (v, subst(v))" rather than directly
with "subst(v)".

There is a complication leading to the need to store the "Ref" name
inside "subst" rather than relying on the name of substituted
variable. When sharing variables "x" and "y" are unified they need to
be substituted with the same Ref name; but Term already uses the
notion of order on variables (just string comparison), it will be
natural to add.

Regards.