WIP: Expanded documentation (inc. @gteege's manual) #334

jashank · 2020-01-07T03:56:17Z

this PR substantially expands the Cogent documentation. the result is in two parts:

An Introduction to Cogent, largely based on introductory text that already existed; and
Cogent Reference Manual, largely based on @gteege's manual converted to reStructuredText.

rendered preview: https://cogent--334.org.readthedocs.build/en/334/

jashank · 2020-01-10T04:33:16Z

I've split this PR into two parts --- the majority of the commits (but not the majority of the changes) come from what is now #338; this PR notionally depends on changes introduced there.

Most of the transformation was done automatically with a gnarly mess of Emacs-Lisp, and was cleaned up a bit (especially the custom TeX macros) by hand. This is a temporary location --- I'll be working on folding this into the rest of the manual, copy-editing, etc. [skip ci][skip lemma]

The 'introduction' expands the 'getting started' documentation, a quick installation reference, and the first programs. The 'reference' is intended to combines the previous (proto-reference) documentation with Gunnar Teege's manual, expanding and clarifying them. [skip ci][skip lemma]

[skip ci][skip lemma]

Split up the old 'getting started' page; the examples can be fleshed out some more and cleaned up, which is on the todo list. [skip ci][skip lemma]

[skip ci][skip lemma]

…ASH ^{10}) [skip ci][skip lemma]

[skip ci][skip lemma]

…SQUASH ^{13}) [skip ci][skip lemma]

[skip ci][skip lemma]

…. (SQUASH ^{17}) [skip ci][skip lemma]

[skip ci][skip lemma]

…SH ^{22}) A gentle, step-wise introduction to the `add' function unfolds, where we build up the language's capabilities piecewise. Instead of diving into a polymorphic type definition, let's start with a very simple function, and build from there. [skip ci][skip lemma]

…{23}) [skip ci][skip lemma]

[skip ci][skip lemma]

Based on discussions with Peter Chubb, some of my own experiments to clarify behaviours, and presented here for first review. Much, much more work is needed, of course. [skip ci][skip lemma]

Includes changes derived from feedback from Louis Cheung -- thanks!

zilinc · 2020-10-08T01:30:26Z

docs/reference/antiquoted-c.rst

+and there are several quotation types:
+
+- ``$id:(IDENT)`` introduces ``IDENT`` as an identifier;
+- ``$ty:(TYPE-NAME)`` refers to the type ``TYPE-NAME``;


It's not necessarily a "type name". It can be any type, including the parameterised ones, like $ty:(Array t).

zilinc · 2020-10-08T01:39:11Z

docs/reference/antiquoted-c.rst

+- ``$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


The purpose of this antiquote is not for typecasting. It only uses typecast's syntax, but the generated C code will be a higher-order function application. The entire antiquoted C mechanism uses the antiquotation is the Haskell C parser, repurposed. Thus we have to choose antiquotes that already exist in the C parser, and they should make sense intuitively. In this case, the typecast antiquote is the best that I can find that makes some sense (that there is one dispatch function for each function type A -> B and that's the "spec" for us to choose which dispatch function to invoke), but apparently less so compared to the others like $ty or $exp.

zilinc · 2020-10-08T01:41:53Z

docs/reference/antiquoted-c.rst

+Quotation types influence this transformation,
+and there are several quotation types:
+
+- ``$id:(IDENT)`` introduces ``IDENT`` as an identifier;


It doesn't quite introduce an identifier. It "instantiates" a polymorphic function/type's name. So we only need to use $id when the function/type is polymorphic, so that it can derive the monomorphised name.

zilinc · 2020-10-08T01:46:57Z

docs/reference/antiquoted-c.rst


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


I'm not quite sure if antiquoting U8 or U32 are good examples. Usually these type don't need antiquotation at all. We know that they become u8 and u32 defined by the stdlib. I'm afraid it will mislead users to use them this way and lead to a more verbose antiquoted C.

my intent here (and, indeed, in most of this rewrite) is to introduce each specific element relatively carefully and clearly: exemplifying the syntax via trivially simple examples before getting to more complex (and realistic) examples feels (to me) to be a good way to introduce this, and my eventual goal is to provide more reference description. I posit the example of the trivial Cogent type U8 being transformed into the C type u8 is what I want to illustrate here. I will add some more words to suggest this is highly unusual to see, though.

Alternatively you can just be vague about the type, say T (we don't even need to know what it is, as long as it's used in the Cogent program), if you think it still keeps the matter simple for your purpose.

Thinking about it twice, antiquoting primitive types isn't that bad, or at least I shouldn't feel bad about it, as I never complain about the verbosity of the antiquoted C files.

zilinc · 2020-10-08T01:50:36Z

docs/reference/antiquoted-c.rst


+  type Result t e = < Ok t | Err e >


I think better examples would be to use the structural types in antiquotes directly (e.g. $ty:((U32, U8))). Type names aren't really a thing in Cogent's structural type system, they gets desugared away very early in the compilation. I would like the doc to discourage users to focus on type synonyms too much.

zilinc · 2020-10-08T01:53:44Z

docs/reference/antiquoted-c.rst

+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.


Maybe be a bit more explicit: the Cogent type appearing in antiquotes have to be types that already get used in the Cogent code ("used" means that it not only appears in the code, but also used by the entry-point functions or their dependencies.

And a common troubleshooting: if it generates a new C type name t42 but without the definition of it, it's usually because some new Cogent type is used in the antiquote.

zilinc · 2020-10-08T01:56:43Z

docs/reference/antiquoted-c.rst

+
+Antiquoted C introduces an *antiquote*,
+which takes the form
+``$``, quotation type, ``:``, and a (usually parenthesised) term;


If it's a single word starting with lowercase, then no parens are needed. It's still useful to reduce the verbosity. On the other hand, if it antiquotes a tuple, then at least two pairs of parens are needed, one for the antiquote, and one for the tuple.

zilinc · 2020-10-08T02:05:53Z

docs/reference/antiquoted-c.rst

+``$esc`` and ``$escstm``: No Escape In Sight
+--------------------------------------------
+
+``$esc:(PREPROCESSOR-DIRECTIVE)`` and


The thing inside the $esc and $escstm doesn't have to be a cpp directive. It can be anything that the user doesn't want the Cogent compiler to see. The only different is that $esc is top-level, and $escstm is on the statement level. The only criterion is that if you remove the entire $esc and $escstm` antiquotes, the rest should still be valid antiquote C.

zilinc added documentation WIP labels Jan 8, 2020

jashank requested a review from zilinc January 10, 2020 04:33

jashank force-pushed the docs-import-manual branch from 5f8dd18 to 85c55a0 Compare January 10, 2020 06:57

jashank force-pushed the docs-import-manual branch 2 times, most recently from cf29dc8 to b9e2ae0 Compare February 13, 2020 06:18

jashank removed the request for review from zilinc February 13, 2020 06:19

jashank changed the title ~~WIP: Port Gunnar Teege's manual to reST, to fold into the manual.~~ WIP: Expanded documentation (inc. @gteege's manual) Feb 13, 2020

jashank force-pushed the docs-import-manual branch 3 times, most recently from cf69c6d to 2b81607 Compare February 14, 2020 08:14

vjackson725 force-pushed the master branch from 21b81a5 to eebf066 Compare March 9, 2020 02:44

jashank force-pushed the docs-import-manual branch from 57dec82 to a6597d8 Compare April 7, 2020 05:53

jashank force-pushed the docs-import-manual branch 3 times, most recently from 5233f89 to 2a21bc0 Compare May 1, 2020 06:28

jashank force-pushed the docs-import-manual branch from 80b66cd to a6166cf Compare September 16, 2020 12:23

jashank added 12 commits October 7, 2020 14:17

docs: Use the documentation tree's symlink. (SQUASH ^^)

f7d1a4c

[skip ci][skip lemma]

docs: Lose the first-page header. (SQUASH ^{3})

bbde6d4

[skip ci][skip lemma]

docs: Promote the \chapter's to \part's in the LaTeX docs. (SQUASH ^{4})

bfd90f8

[skip ci][skip lemma]

docs: Mark the appendices for the LaTeX output. (SQUASH ^{5})

13ed8f1

[skip ci][skip lemma]

docs: Rearrange the "introduction" section. (SQUASH ^{6})

78cd4d6

Split up the old 'getting started' page; the examples can be fleshed out some more and cleaned up, which is on the todo list. [skip ci][skip lemma]

docs: Shuffle the syntax documents; fix broken references. (SQUASH ^{7})

d2ceed6

[skip ci][skip lemma]

docs: README to reST; add some structured project info (SQUASH ^{8})

88d40de

[skip ci][skip lemma]

docs: intro/install: point at the full installation instructions (SQU…

09a7445

…ASH ^{10}) [skip ci][skip lemma]

docs: `preamble' has been teased apart. (SQUASH ^{11})

8b1bb4f

[skip ci][skip lemma]

docs: Extract @gteege's "this is not a tutorial" wording. (SQUASH ^{12})

a598ed6

[skip ci][skip lemma]

jashank added 21 commits October 7, 2020 14:18

docs: ref/syntax: merge @gteege's syntax docs in as surface syntax. (…

ae52010

…SQUASH ^{13}) [skip ci][skip lemma]

docs: ref/core: Import liamoc fig 3.1. (SQUASH ^{13})

071b000

[skip ci][skip lemma]

docs: Use the magic |cogent| macro. (SQUASH ^{14})

547ff88

[skip ci][skip lemma]

docs: ref/values: intro, patterns (SQUASH ^{15})

3729508

[skip ci][skip lemma]

docs: ref/compiler: Clean up sectioning. (SQUASH ^{16})

7fd9236

[skip ci][skip lemma]

docs: appx/todo: Do something with all those `.todo's floating around…

779eb65

…. (SQUASH ^{17}) [skip ci][skip lemma]

docs: Use the small-caps Cogent runes more often. (SQUASH ^{18})

a79a1af

[skip ci][skip lemma]

docs: ref/types: Style cleanup; spelling, grammar. (SQUASH ^{19})

af353f8

[skip ci][skip lemma]

docs: Use reST's xref syntax. (SQUASH ^{20})

00d3691

[skip ci][skip lemma]

docs: intro/first-program: working through content. (SQUASH ^{21})

ad3f25b

[skip ci][skip lemma]

docs: intro/first-program: Fix the branches; promote a par. (SQUASH ^…

e06b33f

…{23}) [skip ci][skip lemma]

docs: intro/first-program: Gentler introduction to AqC.

ceb0b73

[skip ci][skip lemma]

docs: shunt old documentation out of the way.

129db3c

[skip ci][skip lemma]

docs: Bump version numbers in documentation.

1fa5f62

[skip ci][skip lemma]

docs: Fix path to the Cogent logo.

08f1cbd

[skip ci][skip lemma]

docs: reference/surface-syntax: note identifier moves.

05a5e33

[skip ci][skip lemma]

docs: introduction/first-program: Clean up some language.

0b88c12

[skip ci][skip lemma]

docs: Move the Antiquoted C documentation out of the way.

c666169

[skip ci][skip lemma]

docs: A first draft of a first draft of new AqC docs.

3049739

Based on discussions with Peter Chubb, some of my own experiments to clarify behaviours, and presented here for first review. Much, much more work is needed, of course. [skip ci][skip lemma]

docs: reference/antiquoted-c: Expand some of the description.

f5dc7f1

Includes changes derived from feedback from Louis Cheung -- thanks!

jashank force-pushed the docs-import-manual branch from 3e0764a to f5dc7f1 Compare October 7, 2020 03:18

zilinc reviewed Oct 8, 2020

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

WIP: Expanded documentation (inc. @gteege's manual) #334

WIP: Expanded documentation (inc. @gteege's manual) #334

jashank commented Jan 7, 2020 •

edited

Loading

jashank commented Jan 10, 2020

zilinc Oct 8, 2020

zilinc Oct 8, 2020

zilinc Oct 8, 2020

zilinc Oct 8, 2020

jashank Oct 15, 2020

zilinc Oct 15, 2020

zilinc Oct 15, 2020

zilinc Oct 8, 2020

zilinc Oct 8, 2020

zilinc Oct 8, 2020

zilinc Oct 8, 2020

zilinc Oct 8, 2020


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

WIP: Expanded documentation (inc. @gteege's manual) #334

Are you sure you want to change the base?

WIP: Expanded documentation (inc. @gteege's manual) #334

Conversation

jashank commented Jan 7, 2020 • edited Loading

jashank commented Jan 10, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jashank commented Jan 7, 2020 •

edited

Loading