How do I ensure a record's discriminant value is equal to another record component's value?

Question

I have a File_Reader composed of two records, File and Buffer. I would like to ensure both Records always have a valid buffer size when initialized, i.e. Data_File.IO_Buffer_Size is equal to Data_In.Size.

I couldn't find a way of initializing a record component's value with another record's component value or discriminant, so I figured I would at least apply a static predicate which was unsuccessful. Using dynamic predicate as,an alternative poses issues in a LightRuntime environment.

I could easily add a Buffer_Size discriminant to File_Reader, but I would like to explore alternative solutions. Lastly, the record layouts must be preserved since they are memory mapped using representation clauses which are not shown:

type File is 
   record
      Name           : String;
      IO_Buffer_Size : Buffer_Size;
   end record; 

type Buffer(Size : Buffer_Size := 300)  is         
   record
      Pos   : Buffer_Size := 0;
      Value : String(1 .. Size);
   end record;

type File_Reader(Name : String) is 
   record        
       Data_In      : Buffer;    
       Data_File    : File := (Name, Data_In.Size); -- Won't work
   end record;

Answer 1

The code you show has some other errors, so it cannot be your actual code if your actual code has only the error you talk about.

First, type File is not valid because the component File.Name is a String, which is an unconstrained array type which is not allowed for a component of a record. You may want to replace this with some bounded String subtype or with Unbounded_String (but trying to make a representation clause for Unbounded_String would be difficult and seems non-sensical).

Second, type File_Reader is not valid because it has a discriminant (File_Reader.Name) of type String, which is a composite type and so not allowed for a discriminant.

Now about your actual problem. If you do not provide File_Reader with a Buffer_Size discriminant, the size of the buffer (File_Reader.Buffer) will always be 300 (or whatever the default value of Buffer.Size is) so you could just as well define that value as a constant and use it in both type Buffer and to initialize File_Reader.Data_File.IO_Buffer_Size. (By the way, I don't understand the purpose of File.IO_Buffer_Size: you can't get to the buffer from a File (you need a File_Reader) so what could File.IO_Buffer_Size be used for?)

In summary, my advice is to add a Buffer_Size discriminant to File_Reader.