idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.51k stars 374 forks source link

Nested Structs in FFI not read correctly #36

Open edwinb opened 4 years ago

edwinb commented 4 years ago

Issue by vfrinken Tuesday Mar 24, 2020 at 04:39 GMT Originally opened as https://github.com/edwinb/Idris2-boot/issues/238


If I have 2 structs in C

typedef struct{
    int * a;
    int b;
    int * c;
}ExtraStruct;

typedef struct{
    ExtraStruct extra;
    int x;
    int y;
} TestStruct;

TestStruct * getTestStruct(){
    TestStruct * ts = (TestStruct*)malloc(sizeof(TestStruct));
    ts -> x = 1234567890;
    ts -> y = -1;
    return ts;
}

and corresponding types in idris

ExtraStruct : Type
ExtraStruct = Struct "ExtraStruct" [("a", Int), ("b", Int), ("c", Int)]

TestStruct : Type
TestStruct = Struct "TestStruct" [("extra", ExtraStruct), ("x", Int),  ("y", Int)]

I'm not able to read the correct values from an instance of TestStruct using a show function like this

Show TestStruct where
  show ts =
      let x : Int = getField ts "x"
          y : Int = getField ts "y"
      in
      "x: " ++ (show x) ++ ", y: " ++ (show y)

Steps to Reproduce

And example is here https://github.com/vfrinken/nestedStructsIdris2.git

Expected Behavior

x: 1234567890, y: -1

Observed Behavior

x: 0, y: 1234567890

edwinb commented 4 years ago

Comment by edwinb Friday Mar 27, 2020 at 20:51 GMT


The strange behaviour is probably because in TestStruct, ExtraStruct isn't a pointer. A Struct on the Idris side needs to be a pointer to the struct on the C side. However, there's no way of checking this when generating the Chez Scheme.

lemunozm commented 4 months ago

Hi, I'm experiencing the same issue modeling a similar pattern.

What's the canonical way of dealing with nested structs? Is there any way to indicate in the Struct fields that the given field must be treated as value instead of a pointer?