saw-core typechecking debugging

[jpaykin]

This branch adds debugging information to saw-core typechecking errors. It adds a new constructor to the TCError data structure, called ErrorTerm, which keeps track of the term in which an error resides. The error message displays this term to provide context to the error. This means that instead of messages like

Inferred type
  sort 1
Not a subtype of expected type
  sort 0
For term
  sort 0

We will now produce error messages of the form

In term
  Prelude.LRT_Fun
  sort 0
  (\(arg4 : sort 0) ->
     let { x@1 = Prelude.BVVec 64 arg0
                   (Prelude.BVVec 64 arg1 (Prelude.Vec 64 Prelude.Bool))
         }
      in Prelude.LRT_Fun
           x@1
           (\(p0' : x@1) ->
              Prelude.LRT_Fun
                #(-empty-)
                (\(p1 : #(-empty-)) ->
                   Prelude.LRT_Fun
                     #(-empty-)
                     (\(p2 : #(-empty-)) ->
                        Prelude.LRT_Fun
                          #(-empty-)
                          (\(p3 : #(-empty-)) ->
                             Prelude.LRT_Fun
                               #(-empty-)
                               (\(p4 : #(-empty-)) ->
                                  Prelude.LRT_Fun
                                    #(-empty-)
                                    (\(p5 : #(-empty-)) ->
                                       Prelude.LRT_Fun
                                         arg4
                                         (\(p6 : arg4) ->
                                            let { x@2 = Prelude.Vec 64
                                                          Prelude.Bool
                                                }
                                             in Prelude.LRT_Ret
                                                  (Prelude.BVVec 64 arg0
                                                     (Prelude.BVVec 64 arg1
                                                        x@2) * x@2)))))))))
Inferred type
  sort 1
Not a subtype of expected type
  sort 0
For term
  sort 0

There are several avenues for potentially improving this feature if needbe:

1. Make ErrorTerm controllable by a debugging flag
2. Before printing an ErrorTerm, check the size of the term; if it is so big that printing the term would not be useful, consider eliding the term, possibly printing its type
3. Raise the ErrorTerm for a different set of terms. Currently it will be raised for any expression called via typeInferComplete, which skips many recursive cases that call typeInfer.

[eddywestbrook]

@brianhuffman what do you think of this change? We are waiting for your thumbs up or thumbs down on it.

[brianhuffman]

Looks reasonable to me.