Add a resugaring extension for Pulse

[mtzguido]

Using FStarLang/FStar#4068, add a resugaring pass to detect pulse computation types and print them in a nicer way. Example:

fn test (x : ref int)
  requires x |-> 'v
  returns  old : int
  ensures  x |-> ('v + 1) ** pure (old == old)
{
  let old = !x;
  x := !x + 1;
  old
}

Now outputs:

* Info at Print.fst(15,0-15,11):
  - Term
    Print.test
    has type
    x: Pulse.Lib.Reference.ref Prims.int
      -> fn
           requires x |-> 'v
           returns x : Prims.int
           ensures x |-> ('v + 1) ** Pulse.Lib.Core.pure (x == x)

Note that there is a bad shadowing of x in the postcondition. This seems difficult to fix (x is ppname_default).

[mtzguido]

cc @amosr-msft, you may find this useful to resugar Co3.

[amosr-msft]

that's fantastic, thanks @mtzguido!