Re: [Toss-devel] New Speagram: terms with sharing

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

Hi.

> I don't have a vision of how Toss specifications should look like, so
> I don't see short-term benefits. I'll finish basing rewriting on
> ISA-matching (it only needs revision of associating rules with
> functors), and expose Greatest Lower Bound so that the implemented
> machinery is available for use; leaving only the explicit sharing and
> term<->structure translations not implemented.

This looks nice - it will finish the term part without sharing, right?
But the next step I was talking about does not require any vision
at all. I meant exactly replacing the current FormulaParser with Term,
i.e. just writing a trs specification for formulas, a function to get them
back in ocaml, and actually replacing the parser with Term.
What do you think about that?

Lukasz