Embedded terms

[robrix]

• Implements the embedding of Swift values into Manifold terms.
• Adds a String module which embeds Swift’s strings into Manifold.
• Embed functions producing terms?
• Evaluate functions at runtime.
• Test that the String.toList function behaves correctly.
• Add a String.fromList function.
• Test that the String.fromList function behaves correctly.
• Fixes Evaluation (& substitution?) produces ill-typed normal forms #175.

[robrix]

This is incorrect.

We evaluate this function when the value term is constructed, not when the defined toList term is evaluated. Therefore, it always fails the guard clause, produces itself in neutral form, and diverges during evaluation.

[robrix]

String.fromList introduces some difficulty:

1. Embedded terms can close over variables without making them visible to maxBoundVariable. This means that Embedded terms can hide their operands when used within constructed lambdas.
2. As a partial workaround, substitution of a variable i can be skipped inside the body of a lambda binding the same variable, i.e. the addition of shadowing semantics. (This is only a partial workaround because Embedded terms can be applied to both the inner and outer bound variables which might incorrectly be assigned the same binding.)
3. The partial workaround described above causes Sigma.second to be judged to be ill-typed. Evidently it depends on shadowing.

[robrix]

This branch exposes (but does not introduce) #178 by means of its fix to #175. We can resolve this by means of unification, but that will be done on another branch.