Support for interfaces with Pulse

[nikswamy]

Interfaces and Pulse

Currently, a Pulse definition cannot be hidden in a module and only its signature visible in an interface. This is not specific to Pulse: The DSL mechanism doesn't yet allow this.

As we start building more useful Pulse libraries, we need a way to have them work with interfaces.

One possibility:

The current implementation of splice_t doesn't check anything: it simply takes the well-typed program produced by the DSL checker and slaps it into the module.

Instead, when splicing in a let f : t' = e into the program, it could check if a val f : t exists, and if so, check that t' <: t

@mtzguido mentioned that instead of this, there could be a new tactic primitive for splicing in well-typed solutions to goals, which could handle this scenario smoothly.

We should also add syntax for writing Pulse signatures, for use mainly in interfaces, i.e., you could write

fn f (...) 
 requires ..
 returns ...
 ensures ...

i.e., a fn without a body, where it gets elaborated to a val f ...