[DMS-48] motoko-san: ADT encoding for tuples

[int-index]

• Dynamically generate the prelude
• Collect tuple arities used in the program
• Encode tuples with ADTs instead of Refs

The new encoding is more suitable for storing tuple in arrays, which will be implemented in a follow-up patch.

[GoPavel]

Looks good to me, but I am pondering about perspectives and alternative implementation of "tuple arity analysis":

So now you have spread everywhere ctxt and mostly into tr_typ function. Later (DMS-52) we will need also gather all instances of tuple type e.g. collect { Tup2[Int, Bool], Tup1[Int] } to add field: tup$2$int$bool; field tup$1$int; into prelude. So I think we can reuse you changes e.g. change IntSet into str Set.t.
(Indeed, we need to support arrays of tuples.)

However I am thinking can we decouple this somehow via using visitor pattern and traverse.ml? Namely, make a function that visit all expressions and types seeking Tuples and gather all instantiations into set. Then via this set we can generate necessary prelude piece.

WDYT?

[int-index]

So I think we can reuse you changes e.g. change IntSet into str Set.t.

Yes, that's the plan, except I think we'll need a typ StrMap.t instead of a str Set.t because the fields are typed, e.g.

field $option_bool: Option[Bool]

It's not enough to collect that $option_bool was used in the translation, we also need to know that it corresponds to Option[Bool].

However I am thinking can we decouple this somehow via using visitor pattern and traverse.ml?

If we wanted to decouple, that'd be a reasonable solution, but I think coupling makes sense here. The principle I used in trans.ml is "whenever we emit code that uses a tuple of arity N, register this in the IntSet", e.g.

  | M.TupE es ->
      let n = List.length es in
      ctxt.tuple_arities := IntSet.add n !(ctxt.tuple_arities);
      !!(CallE (tup_con_name n, List.map (exp ctxt) es))

When we emit CallE (tup_con_name n, ...), we need to know that the prelude will have a declaration for tup_con_name n. And we know it because we update ctxt.tuple_arities on the previous line.

If we decouple computing tuple_arities and Viper code generation, then it's harder to ensure that they stay in sync.

[GoPavel]

<..> I think we'll need a typ StrMap.t instead of a str Set.t because the fields are typed, e.g.

Yes, of course you're right.

If we decouple computing tuple_arities and Viper code generation, then it's harder to ensure that they stay in sync.

Yeah, I agree that it makes sense to keep things sync. However I don't see here any corner case: we modify tuple_arities when we encounter T.TupleT or M.TupE or M.ProjE which only constructors related to tuples. Function arguments probably require some caution?

Also I have thought that probably decoupled version could be easier reused for other types encoded as polymorphic domain/adt e.g. Option[T]. We can express it as a function that collect all types from the unit (instead of just tuple instances). Then we can process this collection and for each element deduce additional definitions we need in the prelude.

Synchronization between prelude and unit translation will be ensured by invariant that type of any subexpression should be visited and presented in the type collection.

Does it make sense? I am not insisting, just trying to find best design to avoid refactoring work in future.
Maybe current version is more in style of the code. For example, further, we can just add this type collection into ctxt

[int-index]

Does it make sense? I am not insisting, just trying to find best design to avoid refactoring work in future.

Alright, so just for the sake of a comparison, I implemented a separate traversal in bd74790.

An interesting discovery is that it generates more declarations than required. I guess it happens because in Motoko, function arguments are packed in tuples, whereas in Viper we use multi-argument functions. Based on this I am now more confident in proceeding with the current solution, i.e. doing translation and collecting tuple arities in one integrated pass. It is more precise this way.

[GoPavel]

Okay, then let's stay with current solution.