TODO

* Rename AST into ParseTree (or similar)

* Define a [Sampling] type-class

We can sample streams and histories. We would like to do so using a
single, common notation.

* Remove [sem_var_instant]

It's not really a semantic rule.

* Grep for "XXX:"  and "TODO:"
* Use type classes for predicates

Example: Is_free_*, Is_Defined_*, Is_Variable_*, clk_

* Prove the characterizing equivalence of [memories]

Cf. [NLustre/Memories.v]

* Follow consistent naming

Follow the 'Implicit Type' declarations

* [Is_present_in] and [Is_absent_in] might not be necessary

Cf. branch 'dumb' for a construction that does not require a dedicated
inductive predicate.

* [equiv_env] is misleading

It is not an [equivalence], rather a [faithful] map.

* Allocate explicit identifiers to node instances.

Currently, the instance name of a node application
[y0, ..., yn = f(e0, ..., em)] comes from the first result variable, i.e.,
[y0].
This approach has two disadvantages.

(1) There is no way to translate calls with no return values.

(2) translate_eqn uses [hd Ids.default ys] which necessitates awkward lemmas
    and conditions to rule out the default case, e.g.,
    [not_Is_Defined_in_eq_stmt_eval_mobj_inv] and [non_trivial_EqApp].