Define a complex-data message-structure that's got a component who's type depends on the value in an earlier defined component.

complex_data_variants.ivy

#lang ivy1.7

include stream              # for bv_codec(), stream, etc. 
include enum_object_codec   # for enum_codec()
include control_packet      # for control-type , family-type


instance packetload : bit_vector(16)
instance packet_codec : bv_codec(packetload, 2)         # 2 bytes

instance control_codec : enum_codec(control, 8)         # 8 bits

# Dependent type encoder/decoder
instance family1_codec : enum_codec(family.family1, 8)         # 8 bits 
instance family2_codec : enum_codec(family.family2, 8)         # 8 bits


object data = { 

    object datagram = {
        type this = struct{
            load1 : packetload,
            load2 : packetload,
            load3 : control,
            load4 : family
            }

    }

 # instantiate codecs for various types occuring in header




    # Encode a TCP datagram into a raw byte stream

    action decode(raw:stream) returns (dgram:datagram) = {
        require raw.end >= 5;
        #require raw.end = 5;
        dgram.load1 := packet_codec.decode(raw,0);
        dgram.load2 := packet_codec.decode(raw,2);
        
        #var load3byte := raw.value(4);  # Obtains a byte
        var load3Stream := raw.segment(4,5);  # Obtains a byte

        # Translate between Stream and BV[8]
        #dgram.load3 := interpretAsEnum(load3byte);
        dgram.load3 := control_codec.decode(load3Stream);

        if (raw.end > 5){
            var load4Stream := raw.segment(5,raw.end);
            var load4 : family;
            if (dgram.load3 = control.msg1){
                load4 := family1_codec.decode(load4Stream);
            } else if (dgram.load3 = control.msg2){
                load4 := family2_codec.decode(load4Stream);
            };

            dgram.load4 := load4; 
        };

        call test(dgram);
    }




     before encode(dgram:datagram) returns(raw:stream){
     # what are the ways in which we can constrain the creation of an arbitrary datagram? 
     # if the value of dgram.load3 is of a specific value, we intend to generate
        if _generating{

            require (dgram.load3 = control.msg1) -> (dgram.load4 isa family.family1);
            require (dgram.load3 = control.msg2) -> (dgram.load4 isa family.family2);  

            var f:= dgram.load4;
            assert
                (exists (X:family.family1) (f *> X)) |
                (exists (X:family.family2) (f *> X));

            if some (a:family.family1) dgram.load4 *> a{
                assert dgram.load3 = control.msg1;
            };

            if some (a:family.family2) dgram.load4 *> a{
                assert dgram.load3 = control.msg2;
            };


            # --- previous aattempts
            #if (dgram.load3 = control.msg1) {
            #    require (dgram.load4 isa family.family1);
            #    #var load4 : family1; 
            #    #dgram.load4 = load4;
            #    dgram.load4 := family.family1;
            #
            #}else if (dgram.load3 = control.msg2) {
            #    #require dgram.load4 : family2;
            #    #var load4 : family2; 
            #    #dgram.load4 := load4            
            #    dgram.load4 := family.family2;
            #    require (dgram.load4 isa family.family1);
            #}
            #dgram.load4 = load4
                
        }
     }


    action encode(dgram:datagram) returns (raw:stream) = {

        call test(dgram);

        # 4 bytes to represent the packetloads
        raw := raw.resize(4,0);
        raw := packet_codec.encode(raw,0,dgram.load1);
        raw := packet_codec.encode(raw,2,dgram.load2);
        call show_stream(raw);
        
        # -------------------------------
        # How to serialize the enumerated data-type? 
        # raw := control_codec.encode(raw,4,dgram.load3);        # Doesn't work. 

        #var load3 := interpretAsByte(dgram.load3);
        #raw := raw.set(4,load3);

        var load3 := control_codec.encode(dgram.load3);
        call show_stream(load3);
        raw := raw.extend(load3);                               # Extending the earlier RAW by as many bytes!

        # -------------------------------
        # Handling the Dependent Data-Type

        if (dgram.load3 = control.msg1){
            assert (dgram.load4 isa family.family1);
            var load4 := family1_codec.encode(dgram.load4);        
            call show_stream(load4);
            raw := raw.extend(load4);                          # Extending the earlier RAW by as many bytes!
        } else if (dgram.load3 = control.msg2){
            assert (dgram.load4 isa family.family2);
            var load4 := family2_codec.encode(dgram.load4);        
            call show_stream(load4);
            raw := raw.extend(load4);                          # Extending the earlier RAW by as many bytes!
        }


    }


   


    import action test(x:datagram) #= {};
    import action show_stream(y:stream) #= {};
}


attribute radix=16