Typecheck two PIR files

[florentc]

This PR adds partial support for Plutus IR primitives to progress on #88. Development is guided for now by running pirouette on the split and auction validators.

• typing: this PR provides typing for the constants, and a subset of builtins including those used by the auction validator. Testing is not possible until #101 is solved.
• conversion to SMT lib: this provides support for basic builtins on integers and strings, enough for the split validator. The remaining translations for builtins used by auction (lists and data) are listed and remain to be implemented

---

edit by @VictorCMiraldo:

• This PR was downsized to simply typechecking and symbolically executing two golden PIR files (auction.flat and split.flat) that come from our plutus-libs repo
• Moreover, it also handles the type-dependencies of let-bindings floated to the top level

[VictorCMiraldo]

I just merged #103 into dev, then dev into here and I could see the type-checking problems, which shows that the types of certain builtins is probably wrong. This PR is good to go as soon as the tests pass; I'll mark it as ready for review.

[VictorCMiraldo]

We currently have a bug w.r.t the translation of dependencies of terms brought from within a let statement; check the definition of go2339:

go2339 |->
  2#k2300 -> (2#k2300 -> 2#k2300 -> Bool1980) -> 1#v2301 -> (List2008 (Tuple22015 2#k2300
                                                                                  0#r2302)) -> (These2212 1#v2301
                                                                                                          0#r2302)

It references a number of bound type variables, but these are not being properly declared: it should read something like:

go2339 |->
  ∀ (k2300 : *) (v2301 : *) (r2302 : *)
  2#k2300 -> (2#k2300 -> 2#k2300 -> Bool1980) -> 1#v2301 -> (List2008 (Tuple22015 2#k2300
                                                                                  0#r2302)) -> (These2212 1#v2301
                                                                                                          0#r2302)

We extensively fixed bugs like this when we were still translating to TLA+, so I'll investigate whether this was introduced in #103 tomorrow.

[VictorCMiraldo]

The bug was present before #103 was merged; I can reproduce it on fe7524bcbf23c0a98804408c5ec7f03454712cb5

[VictorCMiraldo]

The two golden tests for typechecking PIR files are now passing; this PR turned out to be quite important and implemented handling of type dependencies when floating let-bindings to the top-level. Moreover, it also removed the types of all unused PlutusIR primitives. This is because a number of the types that we guessed before were wrong; if we don't know a type, we should throw an error so the user of pirouette doesn't spend time debugging elsewhere.

[florentc]

These were not guessed but taken from the documentation from the source in plutus repo. For instance chooseList https://github.com/input-output-hk/plutus/blob/1f31e640e8a258185db01fa899da63f9018c0e85/plutus-core/plutus-core/stdlib/PlutusCore/StdLib/Data/List.hs#L36 The type there has its second forall for the return type after the arrow of the first list parameter.

For chooseData: https://github.com/input-output-hk/plutus/blob/1f31e640e8a258185db01fa899da63f9018c0e85/plutus-core/plutus-core/stdlib/PlutusCore/StdLib/Data/Data.hs#L30

[VictorCMiraldo]

That's pretty confusing! I think the lines you send me are not the type of chooseList and chooseData, they're an excerpt of System F exemplifying how to use those primitives. In the body of the terms you linked, chooseList and chooseData have types which are consistent with what we currently have on our typeOfBuiltin

[VictorCMiraldo]

I think this PR is in good enough state to be reviewed then merged. Current state of the art is:

• We should now be able write PlutusIR terms with our quasiquoter: [pir| \x : Integer . x + 1 |], although the parser is incomplete, two simple tests shows it seems to be working alright.
• We can type two golden PIR files

I think that this is already quite big of a PR, might be worthwhile to merge before adding tests for symbolically evaluating the two golden files.