Start refining the interface for invoking pirouette on `PlutusIR` (#122)

[VictorCMiraldo]

This PR starts stabbing at #122:

• [x] Removes an explicit mention of a main term in PrtUnorderedDefs and PrtOrderedDefs. This was a technicality from PlutusIR and shouldn't affect the rest of pirouette.
• [ ] ~Define a pirouettePIR for interacting with validators~

After too much pain with figuring out dependencies, it occurred to me that maybe everything PlutusIR specific should fall into plutus-libs! I'll do that on this PR and make sure to define this as pirouette-2.0.0 so I have a commit to depend on for the cabal file in plutus-libs.

---

Turns out this is doing significantly more than just working on the interface. As I'm moving forward I'm fixing a number of bugs. Namelly:

• Removes prtDefOfAnyNamespace as certain constructor might be called the same as their types with the different namespaces. Propagate changes by taking namespaces into account for dependency computation.
• Fix a defunctionalization bug: the engine assumed that term and type variables came from the same index pool, in reality, type variable index 0 is not term variable index 0: this is a proper term: f @0 #0, its a function f applied to the first type variable and the first term variable.
• Adds a PureSMT.Options and a Pirouette.Symbolic.Eval.Types.Options so we can later control options through tasty options, otherwise debugging is a massive pain.
• Adds a LanguagePrelude class with a builtinPrelude method, replacing the builtinTypeDefs from LanguageBuiltins.
• Adds a simple symbolic eval statistics result to proveAny
• Monomorphizes all terms, which makes the original and simpler defunctionalization engine work alright (at least for now)

[VictorCMiraldo]

I'm working with this PR in tandem with https://github.com/tweag/plutus-libs/pull/133, once I get all the pirouette-specific bugs out of the way, I'll merge. I'll make sure to update the description accordingly!

[VictorCMiraldo]

Seems like we're hitting another defunctionalization bug; this is the definition of a lengthy _Apply!!.... function:

(λ (ctx : Closure!!PIRTypeByteString_PIRTypeByteString_Bool)
         (ctx : List (Tuple2 ByteString Integer)) (e6902 : Tuple2 ByteString
                                                                  Integer)
         (xs6903 : List (Tuple2 ByteString Integer)) . Tuple2_match @ByteString
           @Integer
           1#e6902                                                                                               
           @(List (Tuple2 ByteString Integer))                                                          
           (λ (c6905 : ByteString) (ds6906 : Integer)                                                
            . Bool_match (fFoldableNil_cfoldMap!Bool!Tuple2<PIRTypeByteString!PIRTypeInteger> 
                -- HERE!! Note how the CConsMonoid!Bool constructor got a lambda, not a Closure!!Bool_Bool_Bool!
                (CConsMonoid!Bool (λ (eta9615 : Bool) (eta9617 : Bool) . AdditiveMonoid_match!Bool v9613
                                                                                                                     @Bool
                                                                                                                     (λ
                                                                                                                      (v9622 : Bool -> Bool -> Bool)
                                                                                                                      (v9624 : Bool)
                                                                                                                      . 1#v9622 3#eta9615
                                                                                                                          2#eta9617))
                        (AdditiveMonoid_match!Bool v9613
                            @Bool
                            (λ (v9627 : Bool -> Bool -> Bool) (v9629 : Bool)
                             . 0#v9629)))
                    (Closure!!Tuple2<PIRTypeByteString!PIRTypeInteger>_Bool_ctor_1 5#ctx
                        1#c6905)
                    4#ctx)
                @(List (Tuple2 ByteString Integer))
                2#xs6903
                (Cons @(Tuple2 ByteString Integer) 3#e6902 2#xs6903)))

Maybe this comes from the fact that we have nested closures? I think this has to do with the imense boolean mess that we have going on... there is a builtin bool that is printed Bool and a defined bool that is also printed Bool... :(

Regardless, I'd expect defunctionalization to work regardless of which bool we have. Will investigate later

[VictorCMiraldo]

Bingo! Managed to reproduce the issue with a better regression test for defunctionalization!

[VictorCMiraldo]

Fixed one bug, found another!

Defunctionalization of destructors should also change the various type arguments involved; currently we are defunctionalizing the body of the destructors alright, but we fail to rewrite the type of values inside 'Just'. We're getting:

Maybe_match6620 @(ByteString -> BidderInfo7795) whatever @(Maybe6617 BidderInfo7795)
  -- Just case
  (λ ipv12631 : Closure!!PIRTypeByteString_BidderInfo . whatever)
  -- Nothing case
  whatever

But we should get:

Maybe_match6620 @Closure!!PIRTypeByteString_BidderInfo whatever @(Maybe6617 BidderInfo7795)
  -- Just case
  (λ ipv12631 : Closure!!PIRTypeByteString_BidderInfo . whatever)
  -- Nothing case
  whatever

Would be great to have a regression test for that.