The language definition currently has a provision for a DECLARE form
inside a procedure body. We need to find a better name for that, and it
has nothing to do with this note at all.
Something *like* this will be added to the language spec when I can get
a decent link. Please note that I have NOT checked the following for
possible parse ambiguities, and it may need to change to resolve these.
SUMMARY: we need a DECLARE form.
We need a mechanism to accomplish the following:
1. Forward declaration of types so that circular use of reference types
is possible.
2. Type declarations of variables defined elsewhere, e.g. in assembly
language. **This usage is unsafe.**
FORWARD DECLARATION OF TYPES
For forward declaration of type declarations, I propose the syntax:
(declare type-name : ref)
(declare type-name : val)
(declare (type-name 'a 'b ... 'z) : ref)
(declare (type-name 'a 'b ... 'z) : val)
The first two forms say that TYPE-NAME is a type name of arity 0 that
will be defined later in the same module. The second two forms say that
TYPE-NAME is a type name of some arity k (where k is the number of
argument types) that will be defined later in the same module.
Two declarations:
(declare (x 'a 'b) : ref)
(declare (x 'c 'd) : ref)
are identical if
(a) they declare the same type name,
(b) they have the same arity
(c) they are both :ref or both :val
(d) the type variable names agree under alphs
substitution
that is: the formal parameter names of the type parameters are NOT
considered part of the type.
Note that this form does NOT specify whether the type is a union, a
structure, or the result of a DEFTYPE. It specifies only that TYPE-NAME
is in fact the name of a type. This underspecification is intentional.
TYPE DECLARATION OF EXTERNALS
For kernel construction, there exist external symbols whose type must be
declared. Also, it may ultimately be desirable to specify the types of
module members independent of their implementations at some point. The
following *syntax* will work for either purpose. At the moment I'm
thinking about declaring variable names and types for things that are
actually defined in assembly language files in the kernel.
Note that this sort of "external" declaration is unsafe, and introduces
an obligation for inspection that must be satisfied by assurance
evaluation. The form below may be viewed in some sense as documenting
such an obligation.
In any case, I propose that the form
(declare id : type)
should be used for external declarations, where "id" is a BitC
identifier and "type" is a BitC type. The identifier "id" will behave in
all respects as though it were defined by the module containing the
DECLARE form.
In contrast to forward type declaration, this usage of DECLARE does
*not* expect a definition to follow within the same module -- indeed, a
following definition of this form would be an error!
It may be better to use different syntax for this purpose, such as
perhaps
(extern id : type)
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
