Re: [bitc-dev] [SPAM] Re: [SPAM] Re: [SPAM] Re: [SPAM] Re: Bounded Quantification and parametric inference

Sandro Magi Fri, 27 Feb 2015 06:34:47 -0800

I used ObjectHeader in the table because this pseudo-C language supports subtyping. That isn't the case for your extensible records proposal; your proposal would need to either store Objects, or invert the ObjectHeader so it's parameterized over its extension, ie. data ObjectHeader R = ObjectHeader { id : UInt64 | R }, and then obj_table :: ArrayN (forall R. ObjectHeader R) Size.

My original sample code didn't provide for projection of a class type to an underlying field either, I just note that it's needed somehow. We need something like Ada's variant records [1], except where legal access is enforced at compile-time instead of via runtime Constraint_Error.

type ObjectTypes is (Process, Node, ...)
for ObjectTypes'Size use 8

type ProcessNode is array(1..32) of Capability
type ObjectHeader (TypeCode : ObjecTypes, Id : UInt64) is
record
case TypeCode is
    when Process =>
Capabilities : CapNode; ...
    when Node => ...
     ...
end case;
end record;

Sandro

[1] http://www.isa.uniovi.es/docencia/TiempoReal/Recursos/textbook/aps12-4.htm

On 27/02/2015 9:07 AM, Keean Schupke wrote:

From here:

static struct ObjectHeader[] global_obj_table;

You had an array of object headers. Sum tag is stored in "type_code" in the underlying structure. I am assuming we chose an int8 which would be first 'item' in the Object memory layout. It might need an explicit annotation.

Keean,
On 27 February 2015 at 14:03, Sandro Magi <[email protected]> wrote:
There seems to be no relation between ObjectHeaders and Objects. Presumably obj_table should be an array of Objects, not of ObjectHeader? If so, where are you storing the sum tag to distinguish the different cases for Objects?

Sandro

On 27/02/2015 8:55 AM, Keean Schupke wrote:
data ObjectHeader = ObjectHeader {
id :: UInt64

}

data Capability = Capability {

id :: UInt65,

facet :: UInt16

}

data Process = Process {ObjectHeader | cap_node :: ArrayN Capacity 32}

data Objects = P Process | N Node ...

data Global {

obj_table :: ArrayN ObjectHeader Size,

running :: Process

}

kernel_msg_send cap_idx msg = let cap = global.running.cap_node[cap_idx] in

let obj = lookup(global.obj_table, cap.id) in case obj of

(P process) -> ...

(N node) -> ...

Keean.

_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Re: [bitc-dev] [SPAM] Re: [SPAM] Re: [SPAM] Re: [SPAM] Re: Bounded Quantification and parametric inference

Reply via email to