obj T = i:integer and j:string and k:boolean;
obj Results = T*;

var exec_count:integer;
var result:T*;

(*
 * Example of how to populate a tuple universe with bounded quantifiers.
 *)
op PopulateTupleUniverse() =
    forall (i in [1..10])
        forall (j in ["abc", "def", "ghi"])
            forall (k in [true, false])
                (let x:T = {i,j,k}; true);

(*
 * Insrtrumented version of the preceding operation, to see the number of
 * executions and its results.  At present, list concat appears not be working,
 * but the count comes out to the expected 10 * 3 * 2 = 60.
 *)
op PopulateTupleUniverseInstrumented() =
    forall (i in [1..10])
        forall (j in ["abc", "def", "ghi"])
            forall (k in [true, false])
                (let x:T = {i,j,k};
                 set result = result + x;
                 set exec_count = exec_count + 1;
                 true);

> set result = [];
> set exec_count = 0;
> PopulateTupleUniverseInstrumented();
> exec_count;                                -- 60, as expected
> result;                                    -- empty, not as expected

(*
 * Recursive functional version of tuple universe population.  It's
 * instrumented, but even with the instrumentation removed, it's way more
 * complicated than it's worth.
 *
 * It makes a good exercise case for intepreter execution, but it's not a
 * particularly practical way to populate a tuple universe.  There may be
 * someway to simplify it, but I can't see it right now.
 *)
function PopulateTupleUniverseRecursive(
        x:T,
        l1:integer*, l2:string*, l3:boolean*,
        index1:integer, index2:integer, index3:integer,
        lower1:integer, lower2:integer, lower3:integer,
        upper1:integer, upper2:integer, upper3:integer) =
    
    if index3 <= upper3 then (
        set exec_count = exec_count + 1;
        PopulateTupleUniverseRecursive(
            {l1[index1], l2[index2], l3[index3]},
            l1, l2, l3,
            index1, index2, index3 + 1,
            lower1, lower2, lower3,
            upper1, upper2, upper3)
    )
    else
        if index2 < upper2 then (
            set exec_count2 = exec_count2 + 1;
            PopulateTupleUniverseRecursive(
                {l1[index1], l2[index2], l3[lower3]},
                l1, l2, l3,
                index1, index2 + 1, lower3,
                lower1, lower2, lower3,
                upper1, upper2, upper3)
        )
        else
            if index1 < upper1 then (
                set exec_count3 = exec_count3 + 1;
                PopulateTupleUniverseRecursive(
                    {l1[index1], l2[lower2], l3[lower3]},
                    l1, l2, l3,
                    index1 + 1, lower2, lower3,
                    lower1, lower2, lower3,
                    upper1, upper2, upper3)
            )
            else
                nil;

var exec_count2,exec_count3:integer;
> set exec_count = 0;
> set exec_count2 = 0;
> set exec_count3 = 0;
> (let l1 = [1..10];
   let l2 = ["abc", "def", "ghi"];
   let l3 = [true, false];
   PopulateTupleUniverseRecursive(
       {nil, nil, nil},
       l1, l2, l3,
       1, 1, 1,
       1, 1, 1,
       #l1, #l2, #l3);
  );
> exec_count;
> exec_count2;
> exec_count3;