Add separate destructors

[Warbo]

Destructors/projections are allowed to appear in generated code, e.g. Haskell, despite not being defined anywhere. Here's a somewhat contrived example:

(declare-datatypes () ((Nat (Z) (S (p Nat)))))
(define-fun pred ((x Nat)) Nat
  (match x
    (case (Z) Z)
    (case (S y) (p x))))
(check-sat)

The pred function is using p to project out the argument from S. Whilst a human might notice that y is an acceptable alternative to (p x), a machine might not. If we send this through tip --haskell we get:

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE RankNTypes #-}
module A where
import qualified Text.Show.Functions
import qualified Data.Typeable as T
import qualified Prelude as P
data Nat = Z | S Nat deriving (P.Eq, P.Ord, P.Show, T.Typeable)
pred :: forall . () => Nat -> Nat
pred Z = Z
pred (S y) = p (S y)

Notice the p in the last line, which isn't defined anywhere. This makes the code unusable:

$ ghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
Prelude> :load A.hs
[1 of 1] Compiling A                ( A.hs, interpreted )

A.hs:13:14: error: Variable not in scope: p :: Nat -> Nat
Failed, modules loaded: none.

The --add-match option can be used to replace such references with a pattern match, but that loses information and intention. It would be nice if there were something like an --add-destructors option which appends separate destructor functions, for example:

(define-fun destructor-p ((x Nat)) Nat
  (match x
    (case (S y) y)))

I've written some rudimentary code for doing this, although it's written in Racket rather than Haskell. See add-destructor-funcs in https://github.com/Warbo/theory-exploration-benchmarks/blob/45d64c4c57dfb42d6ab55b550ef830616e04053d/scripts/defs.rkt#L878