Add separate (eta-expansions of) constructors

[Warbo]

There is an asymmetry between constructor functions and regular functions, despite both being callable value-level terms. It would be nice if standalone functions could be added which are just eta-expansions of the constructors, so subsequent programs which only support functions would still be able to use (an equivalent of) constructors. For example, given:

(declare-datatypes () ((Nat (Z) (S (p Nat)))))

We'd get:

(define-fun constructor-Z () Nat
  (as Z Nat))

(define-fun constructor-S ((x Nat)) Nat
  (as (S x) Nat))

Note that the as is required for parameterised types, and does no harm for concrete types.

In my case, I'm extracting Haskell definitions during Core compilation, because I've found building with Cabal to be the only reliable way to parse Haskell code (for example, using haskell-src-exts or the GHC API like in tip-ghc, we fail when code requires preprocessing; or we have to guess which extensions, library paths, etc. to include; and so on). Since constructors are uninterpreted symbols, they're never passed to the compilation function, and hence I only see regular functions.

I've written code to do this, although it's in Racket rather than Haskell. See the add-constructor-funcs definition at https://github.com/Warbo/theory-exploration-benchmarks/blob/45d64c4c57dfb42d6ab55b550ef830616e04053d/scripts/defs.rkt#L816