More idiomatic go code

[larsrh]

Currently, Plus_nat is generated as follows:

func Plus_nat(x0 Nat, n Nat) Nat {
  {
    q, m := x0.(Suc)
    if m {
      ma := Suc_dest(q)
      nb := n
      return Plus_nat(ma, Nat(Suc{nb}))
    }
  }
  {
    if x0 == (Nat(Zero_nat{})) {
      nb := n
      return nb
    }
  }
  panic("match failed")
}

The slightly more idiomatic version would be:

func Plus_nat(x0 Nat, n Nat) Nat {
  if q, ok := x0.(Suc); ok {
    ma := Suc_dest(q)
    nb := n
    return Plus_nat(ma, Nat(Suc{nb}))
  }
  if x0 == (Nat(Zero_nat{})) {
    nb := n
    return nb
  }
  panic("match failed")
}

Main changes:

• Use assignment directly in the condition of the if block.
• Everything is in an if block, so we don't need the surrounding {} blocks to limit scope.
• The variable which checks whether a type assertion was successful is usually called ok.

Reported by @diekmann

[stuebinm]

so point 1 & 3 are very easy to implement; these are only moving the generated code around a little.

However, getting rid of the extra {} blocks in the translation of multi-equation functions is a lot more tricky, since these also have a second purpose: a function may give different names to the same argument in different equations, so we might have to do some renaming. Consider e.g.

fun names :: "'b ⇒ 'a option * 'b option ⇒  'b option" where
  "names b (None, _) = Some b"
| "names s (_, None) = Some s"
| "names s _  = Some s"

where the first argument's name changes between branches:

func Names[a, b any] (ba a, x1 Product_Type.Prod[Option.Optiona[b], Option.Optiona[a]]) Option.Optiona[a] {
  {
    bc := ba;
    ...
  };
  {
    sa := ba;
    ...
  };
  {
    sa := ba;
    ...
  };
  panic("match failed");
}

now if we remove the extra blocks, suddenly we define sa twice, which is an error. But after a couple of tries which went nowhere, i think i found a reasonable solution for this: the above can only happen in multi-equation functions in which (a) we match on more than one argument and (b) at least one of the patterns actually deconstructs something (i.e. does not just assign a name). Also, the patterns for each argument are independent of each other, and the order in which they are checked doesn't matter.

So we can always safely "push inwards" the renamings to an inner layer, and get

func Names[a, b any] (ba a, x1 Product_Type.Prod[Option.Optiona[b], Option.Optiona[a]]) Option.Optiona[a] {
  _ = x1;
  c, _ := Product_Type.Pair_dest(x1);
  if c == (Option.Optiona[b](Option.None[b]{})) {
    bc := ba;
    return Option.Optiona[a](Option.Some[a]{bc});
  }
  _ = x1;
  p, c := Product_Type.Pair_dest(x1);
  if c == (Option.Optiona[a](Option.None[a]{})) {
    if _, ok := p.(Option.Some[b]); ok {
      sa := ba;
      return Option.Optiona[a](Option.Some[a]{sa});
    }
  }
  _ = x1;
  q, p := Product_Type.Pair_dest(x1);
  if _, ok := q.(Option.Some[b]); ok {
    if _, ok := p.(Option.Syome[a]); ok {
      sa := ba;
      return Option.Optiona[a](Option.Some[a]{sa});
    }
  }
  panic("match failed");
}

without any extra {}.

(alternatively, we could also try to unify such variable names across all equations of a function, which gets rid of this entire problem — but that seems error-prone, and so far we've always preferred keeping renamings in the Go code)