Skip to content

Commit

Permalink
docs: reference/antiquoted-c: Expand some of the description.
Browse files Browse the repository at this point in the history 
Includes changes derived from feedback from Louis Cheung -- thanks!
  • Loading branch information
@jashank
jashank committed Oct 7, 2020
1 parent 3049739 commit f5dc7f1
Showing 1 changed file with 147 additions and 85 deletions.
232 changes: 147 additions & 85 deletions docs/reference/antiquoted-c.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,10 @@

.. warning::
Cogent antiquotation has almost no checking.
Be very, very careful, as the result may break.
Be very, very careful,
as it is easy to write invalid constructs
that won't parse or won't compile,
and which are extremely hard to debug.

|cogent| is a substantially restricted language:
many operations cannot be expressed,
Expand All @@ -16,114 +19,173 @@ more capability is required.

*Antiquoted C* is the mechanism by which
we can invoke |cogent| from C.
Antiquoted C behaves
something like a template language:
an *antiquote* take the form
``$``, quotation type, ``:``, and (usually parenthesised) term;
and denotes an item in C that must
be understood, and potentially transformed,
by the |cogent| compiler.
Quotation types influence the way the term is transformed:
For the most part,
Antiquoted C is syntactically identical to C.
However, there are certain constructs
where the underlying C parser
will incorrectly reject otherwise-valid constructs.
But Antiquoted C also behaves
a little like a template language,
and this is what we're interested in.


Antiquotes
====================================

Antiquoted C introduces an *antiquote*,
which takes the form
``$``, quotation type, ``:``, and a (usually parenthesised) term;
and it denotes an item in C that
the |cogent| compiler must understand
and potentially transform.
It is wise to parenthesise the term,
to make it visually evident
it is distinct from the C around it.
Quotation types influence this transformation,
and there are several quotation types:

- ``$id:(IDENT)`` introduces ``IDENT`` as an identifier;
- ``$ty:(TYPE-NAME)`` refers to the type ``TYPE-NAME``;
- ``$exp:(EXPRESSION)`` inserts code to execute ``EXPRESSION``;
- ``$spec:(TYPE-NAME)`` injects an appropriate C typecast; and
- ``$esc:(PREPROCESSOR-DIRECTIVE)`` and
``$escstm:(PREPROCESSOR-DIRECTIVE)``
allow insertion of a literal C preprocessor directive.

- ``$id:(IDENT)`` introduces ``IDENT`` as an identifier
at the point of declaration, either of a function or a type::
We'll look at each of these in detail.

void $id:(stare_into_abyss) (void) { /* ... */ }

struct $id:(by_lightning) { /* ... */ }
``$id``: Introducing Identifiers
------------------------------------

Often, these aren't required:
if no type parameters are involved,
as might be the case with ``stare_into_abyss`` above,
this could be declared without antiquotes.
``$id:(IDENT)`` introduces ``IDENT`` as an identifier
at the point of declaration, either of a function or a type::

void $id:(stare_into_abyss) (void) { /* ... */ }

- ``$ty:(TYPE-NAME)`` refers to the type ``TYPE-NAME``,
which may be any type known to |cogent|.
For example, we could declare a function
that uses C's coercion of U8 to U32::
struct $id:(by_lightning) { /* ... */ }

$ty:(U32) u32_from_u8 ($ty:(U8) x) { return x; }
Often, these aren't required:
if there are no type parameters,
as might be the case with ``stare_into_abyss`` above,
this declaration can occur without antiquotes.

At compilation,
|cogent| will replace the ``$ty`` term with
a corresponding C type,
so the generated result would be::

u32 u32_from_u8(u8 x) { return x; }
``$ty``: Talking Types
------------------------------------

This works for less-trivial types as well.
In |cogent|,
if we declare the types ``Result``, ``FileDesc``, ``Errno``,
and a function of them, ``openf``::
``$ty:(TYPE-NAME)`` refers to the type ``TYPE-NAME``,
which may be any type known to |cogent|,
especially those that include a type parameter
and which C cannot itself express.

type Result t e = < Ok t | Err e >
type FileDesc = U32
type Errno = U32
openf: U32 -> Result FileDesc Errno
For example, we could declare a function
that uses C's coercion of U8 to U32::

We can then implement this function in C::
$ty:(U32) u32_from_u8 ($ty:(U8) x) { return x; }

$ty:(Result FileDesc Errno)
openf ($ty:(U32) arg)
{
/* ... */
}
At compilation,
|cogent| will replace the ``$ty`` term with
a corresponding C type,
so the generated result would be::

This will be transformed into::
u32 u32_from_u8(u8 x) { return x; }

t1 openf(u32 arg) { /* ... */ }

where the type definition ``t1`` has already been generated.
Beware that the |cogent| compiler
may not always emit the type's definition,
even if it emits a reference to it.
This works for less-trivial types as well.
In |cogent|,
if we declare the types ``Result``, ``FileDesc``, ``Errno``,
and a function of them, ``openf``::

type Result t e = < Ok t | Err e >
type FileDesc = U32
type Errno = U32
openf: U32 -> Result FileDesc Errno

- ``$exp:(EXPRESSION)`` inserts code to execute ``EXPRESSION``.
The most common case for this is to call |cogent| functions,
or to access top-level bindings.
We can then implement this function in C::

For example,
if we have a |cogent| function::
$ty:(Result FileDesc Errno)
openf ($ty:(U32) arg)
{
/* ... */
}

within_bounds: U32 -> Bool
within_bounds x = {- ... -}
The compiler will transform this into something like::

Then, if we wish to invoke it from in C,
we might say::
t1 openf(u32 arg) { /* ... */ }

if ($exp:(within_bounds)(value)) { /* ... */ }
where the type definition ``t1`` was previously generated.
Beware that the |cogent| compiler
may not always emit the type's definition,
even if it emits a reference to it.


- ``$spec:(TYPE-NAME)`` will,
if ``TYPE-NAME`` is a function,
insert an appropriate C type;
this is intended for use
when type-casting function pointers,
as is necessary when invoking a lambda.
``$exp``: Embedding Expressions
------------------------------------

``$exp:(EXPRESSION)`` inserts code to execute ``EXPRESSION``.
The most common case for this is to call |cogent| functions,
or to access top-level bindings.

- ``$esc:(PREPROCESSOR-DIRECTIVE)`` and
``$escstm:(PREPROCESSOR-DIRECTIVE)``
allow insertion of a literal C preprocessor directive.
For example,
if we have a |cogent| function::

within_bounds: U32 -> Bool
within_bounds x = {- ... -}

Then, if we wish to invoke it from in C,
we might say::

if ($exp:(within_bounds)(value)) { /* ... */ }


``$spec``: Specifying Casts
------------------------------------

``$spec:(TYPE-NAME)`` will,
if ``TYPE-NAME`` is the type of a function,
insert an appropriate C typecast.
Its most common use is
when type-casting function pointers,
as is necessary when invoking
a function reference passed from |cogent| to C.

As an example,
let's consider a function whose type is


type ArrayModifyF a acc = OptElemA a acc -> OptElemA a acc



``$esc`` and ``$escstm``: No Escape In Sight
--------------------------------------------

``$esc:(PREPROCESSOR-DIRECTIVE)`` and
``$escstm:(PREPROCESSOR-DIRECTIVE)``
allow the insertion of a literal C preprocessor directive.

The most common uses of ``$esc``
are to introduce ``#define``s,
and to work around header files
which use any features
the underlying C parser cannot deal with ---
GNU libc's headers, for example,
are a common case::
$esc:(#include <stdio.h>)
$esc:(#include <stdlib.h>)
``$escstm`` occurs in a statement context;
this is useful, for example,
in combination with
the C preprocessor's conditional construct
to choose between two different implementations
depending on some other influence::

The most common uses of ``$esc``
are to introduce ``#define``s,
and to work around header files
which use any features
the underlying C parser cannot deal with ---
GNU libc's headers, for example,
are a common case::
$esc:(#include <stdio.h>)
$esc:(#include <stdlib.h>)
``$escstm`` is expected to be in a statement context;
so, for example::

$escstm:(#if LINUX_VERSION_CODE < KERNEL_VERSION(4,4,0))
page_cache_release(page);
$escstm:(#else)
put_page(page);
$escstm:(#endif)
$escstm:(#if LINUX_VERSION_CODE < KERNEL_VERSION(4,4,0))
page_cache_release(page);
$escstm:(#else)
put_page(page);
$escstm:(#endif)

0 comments on commit f5dc7f1

Please sign in to comment.