Naming conventions

Makefile

@@ -3,6 +3,7 @@
 MAKEFILE_DIR:=$(dir $(realpath $(lastword $(MAKEFILE_LIST))))
 
 default: build exercises build/tutorial.html build/exercises.zip
+all: default
 
 clean:
 	rm -rf build TAGS
@@ -43,6 +44,10 @@ build/solutions/%: src/examples/%
 build/exercises.zip: $(EXERCISES)
 	cd build; zip -r exercises.zip exercises > /dev/null
 
+WORKING=$(wildcard src/examples/list_*.c)
+WORKING_AUX=$(patsubst src/examples/%, build/solutions/%, $(WORKING))
+temp: $(WORKING_AUX) build 
+#     build/tutorial.html 
 
 ##############################################################################
 # Check that the examples all run correctly 

NAMING-CONVENTIONS.md

@@ -0,0 +1,139 @@
+CN Naming Conventions
+---------------------
+
+This document describes our (Benjamin and Liz's) current best shot at
+a good set of conventions for naming identifiers in CN, based on
+numerous discussions and worked examples.
+
+All the list-related files in src/examples have been converted to this
+convention -- do `ls src/examples/list*` to check it out.
+
+# Principles
+
+- When similar concepts exist in both C and CN, they should be named
+  so that the correspondence is immediately obvious.
+     - In particular, the C and CN versions of a given data structure
+       should have very similar names.
+
+- In text, we use the modifiers _CN-level_ vs. _C-level_ to
+  distinguish the two worlds.
+
+# General conventions
+
+ ## For new code
+
+When we're writing both C and CN code from scratch (e.g., in the
+tutorial), we aim for maximal correspondence between 
+
+- In general, CN identifiers are written in `snake_case` rather than `camlCase`
+
+- C-level identifiers are `lowercase_consistently_throughout`
+
+- CN-level identifiers are `Uppercase_Consistently_Throughout`
+
+- A CN identifier that represents the state of a mutable data
+  structure after some function returns should be named the same as
+  the starting state of the data structure, with an `_post` at the
+  end.
+      - E.g., The list copy function takes a linked list `l`
+        representing a sequence `L` and leaves `l` at the end pointing
+        to a final sequence `L_post` such that `L == L_post`.
+        (Moreover, it returns a new sequence `Ret` with `L == Ret`.)
+
+- Predicates that extract some structure from the heap should be named
+  the same as the structure they extract.  E.g., the result
+  type of the `Queue` predicate is also called `Queue`.
+
+  *Discussion*: There is clearly some potential for confusion, and for
+  this reason Liz prefers using `Queue_at` for the predicate.  On the
+  other hand hand, types don't take an argument and predicates do, so
+  it's easy to disambiguate.  We're going with the lighter alternative
+  for the moment.
+
+## For existing code
+
+In existing C codebases, uppercase-initial identifiers are often used
+for typedefs, structs, and enumerations.  We should choose a
+recommended standard convention for such cases -- e.g., "prefix
+CN-level identifiers with `CN` when needed to avoid confusion with
+C-level identifiers".  Some experimentation will be needed to see
+which convention we like best; this is left for future discussions.
+
+# Built-ins
+
+This proposal may also require changing some built-ins for
+consistency.
+
+      - `i32` should change to `I32`, `u64` to `U64`
+      - `is_null` to `Is_null` (or `Is_Null`)
+
+*Discussion*: One point against this change is that CN currently tries
+to use names reminiscent of Rust (`i32`, `u64`, etc.).  I (BCP) do not
+personally find this argument persuasive -- internal consistency seems
+more important than miscellaeous points of similarity with some other
+language.  One way or the other, this will require a global decision.
+
+# Polymorphism
+
+One particularly tricky issue is how to name the "monomorphic
+instances" of "morally polymorphic" functions (i.e., whether to write
+`append__Int` or `append__List_Int` rather than just `append`).  On
+one hand, `append__Int` is "more correct".  On the other hand, these
+extra annotations can get pretty heavy.
+
+We propose a compromise:
+
+1. If a project needs to use two or more instances of some polymorphic
+   type, then the names of the C and CN types, the C and CN functions
+   operating over them, and the CN predicates describing them are all
+   suffixed with `__xxx`, where `xxx` is the appropriate "type
+   argument".  E.g., if some codebase uses lists of both signed and
+   unsigned 32-bit ints, then we would use names like this:
+      - `list__int` / `list__uint`
+      - `append__int` / `append__uint`
+      - `List__I32` / `List__U32`
+      - `Cons__I32` / `Cons__U32`
+      - etc.
+
+2. However, if, in a given project, a set of "morally polymorphic"
+   type definitions and library functions is *only used at one
+   monomorphic instance* (e.g., if some codebase only ever uses lists
+   of 32-bit signed ints), then the `__int` or `__I32` annotations are
+   omitted.
+
+   This convention is used in the CN tutorial, for example.
+
+   TODO: Right now, the tutorial uses option (1).  It was this
+   exercise that convinced me [BCP] that option (2) was better. :-)
+
+*Discussion*: One downside of this convention is that it might
+sometimes require some after-the-fact renaming: If a project starts
+out using just lists of signed ints and later needs to introduce lists
+of unsigned ints, the old signed operations will need to be renamed.
+This seems like an acceptable cost for keeping things light.
+
+Another downside is that it introduces two different ways of naming
+polymorphic things.  But hopefully (a) the appropriate use of each is
+clear and (b) most C developments will actually fall in the second,
+lighter case, and programmers will never need to bother understanding
+the first case.
+
+# Loose ends
+
+- Do we need a convention for auxiliary predicates?
+    - E.g., maybe adding `_Aux` to the original predicate name
+      (e.g. `Queue_Aux` for the recursive predicate that walks down
+      the list of queue nodes to gather them into a list once a
+      top-level `Queue` or `Queue_at` predicate has dealt with the
+      non-recursive part of the structure).
+
+- The current function `IntList_free__list` is hard to rename with
+  these conventions. It feels like it should be `free__sllist`, but
+  that’s also the new name of the free function for individual list
+  cells (opposite of `malloc`). Current solution is
+  `free_rec__sllist`.
+    - BCP wonders if this issue is specific to malloc and free.  If
+      so, maybe we can make some special convention like
+      `free__sllist_node` for the single-node operation (even though
+      what it returns is an `sllist`, noit an `sllist_node`),
+      leaving `free__sllist` for the recursive one?

src/example-archive/simple-examples/working/malloc_1.c

@@ -3,19 +3,19 @@
 // malloc() is not defined by default in CN. We can define a fake malloc()
 // function that only works on ints.
 
-int *my_malloc_int()
+int *my_malloc__int()
 /*@ trusted; @*/
 /*@ ensures take New = Block<int>(return); @*/
 {}
 
-int *malloc_1()
+int *malloc__1()
 /*@ ensures 
       take New = Owned<int>(return);
       New == 7i32;
       *return == 7i32; @*/  // <-- Alternative syntax 
 {
   int *new;
-  new = my_malloc_int();
+  new = my_malloc__int();
   *new = 7; // Have to initialize the memory before it's owned
   return new;
 }

src/examples/Dbl_Linked_List/add.c

@@ -5,11 +5,11 @@ struct node *add(int element, struct node *n)
 /*@ requires take Before = Dll_at(n);
     ensures  take After = Dll_at(return);
 
-             is_null(n) ? After == Dll { left: Seq_Nil{}, curr: Node(After), right: Seq_Nil{}}
-                        : After == Dll { left: Seq_Cons{head: Node(Before).data, tail: Left(Before)}, curr: Node(After), right: Right(Before)};
+             is_null(n) ? After == Dll { left: Nil{}, curr: Node(After), right: Nil{}}
+                        : After == Dll { left: Cons{Head: Node(Before).data, Tail: Left(Before)}, curr: Node(After), right: Right(Before)};
 @*/
 {
-    struct node *new_node = malloc_node();
+    struct node *new_node = malloc__node();
     new_node->data = element;
     new_node->prev = 0;
     new_node->next = 0;

src/examples/Dbl_Linked_List/add_orig.broken.c

@@ -3,7 +3,7 @@
 // Adds after the given node and returns a pointer to the new node
 struct node *add(int element, struct node *n)
 {
-    struct node *new_node = malloc_node();
+    struct node *new_node = malloc__node();
     new_node->data = element;
     new_node->prev = 0;
     new_node->next = 0;

src/examples/Dbl_Linked_List/cn_types.h

@@ -1,6 +1,6 @@
 /*@
 datatype Dll {
     Empty_Dll {},
-    Dll {datatype seq left, struct node curr, datatype seq right}
+    Dll {datatype List left, struct node curr, datatype List right}
 }
 @*/

src/examples/Dbl_Linked_List/getters.h

@@ -1,14 +1,14 @@
 /*@
-function (datatype seq) Right (datatype Dll L) {
+function (datatype List) Right (datatype Dll L) {
     match L {
-        Empty_Dll {} => { Seq_Nil{} }
+        Empty_Dll {} => { Nil{} }
         Dll {left: _, curr: _, right: r} => { r }
     }
 }
 
-function (datatype seq) Left (datatype Dll L) {
+function (datatype List) Left (datatype Dll L) {
     match L {
-        Empty_Dll {} => { Seq_Nil {} }
+        Empty_Dll {} => { Nil {} }
         Dll {left: l, curr: _, right: _} => { l }
     }
 }

src/examples/Dbl_Linked_List/malloc_free.h

@@ -1,12 +1,12 @@
-extern struct node *malloc_node();
-/*@ spec malloc_node();
+extern struct node *malloc__node();
+/*@ spec malloc__node();
     requires true;
     ensures take u = Block<struct node>(return);
             !ptr_eq(return,NULL);
 @*/ 
 
-extern void free_node (struct node *p);
-/*@ spec free_node(pointer p);
+extern void free__node (struct node *p);
+/*@ spec free__node(pointer p);
     requires take u = Block<struct node>(p);
     ensures true;
 @*/

src/examples/Dbl_Linked_List/node_and_int.h

@@ -3,15 +3,15 @@ struct node_and_int {
   int data;
 };
 
-extern struct node_and_int *malloc_node_and_int();
-/*@ spec malloc_node_and_int();
+extern struct node_and_int *malloc__node_and_int();
+/*@ spec malloc__node_and_int();
     requires true;
     ensures take u = Block<struct node_and_int>(return);
             !ptr_eq(return,NULL);
 @*/ 
 
-extern void free_node_and_int (struct node_and_int *p);
-/*@ spec free_node_and_int(pointer p);
+extern void free__node_and_int (struct node_and_int *p);
+/*@ spec free__node_and_int(pointer p);
     requires take u = Block<struct node_and_int>(p);
     ensures true;
 @*/

src/examples/Dbl_Linked_List/predicates.h

@@ -10,27 +10,27 @@ predicate (datatype Dll) Dll_at (pointer p) {
     }
 }
 
-predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node) {
+predicate (datatype List) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node) {
     if (is_null(p)) {
-        return Seq_Nil{};
+        return Nil{};
     } else {
         take n = Owned<struct node>(p);
         assert (ptr_eq(n.prev, prev_pointer));
         assert(ptr_eq(prev_node.next, p));
         take Right = Own_Forwards(n.next, p, n);
-        return Seq_Cons{head: n.data, tail: Right};
+        return Cons{Head: n.data, Tail: Right};
     }
 }
 
-predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node) {
+predicate (datatype List) Own_Backwards(pointer p, pointer next_pointer, struct node next_node) {
     if (is_null(p)) {
-        return Seq_Nil{};
+        return Nil{};
     } else {
         take n = Owned<struct node>(p);
         assert (ptr_eq(n.next, next_pointer));
         assert(ptr_eq(next_node.prev, p));
         take Left = Own_Backwards(n.prev, p, n);
-        return Seq_Cons{head: n.data, tail: Left};
+        return Cons{Head: n.data, Tail: Left};
     }
 }
 @*/

src/examples/Dbl_Linked_List/remove.c

@@ -11,8 +11,8 @@ struct node_and_int *remove(struct node *n)
              take After = Dll_at(ret.node);
              ret.data == del.data;
              (is_null(del.prev) && is_null(del.next)) ? After == Empty_Dll{}
-                 : (!is_null(del.next) ? After == Dll{left: Left(Before), curr: Node(After), right: tl(Right(Before))}
-                     : After == Dll{left: tl(Left(Before)), curr: Node(After), right: Right(Before)});
+                 : (!is_null(del.next) ? After == Dll{left: Left(Before), curr: Node(After), right: Tl(Right(Before))}
+                     : After == Dll{left: Tl(Left(Before)), curr: Node(After), right: Right(Before)});
 @*/
 {
     struct node *temp = 0;
@@ -27,10 +27,10 @@ struct node_and_int *remove(struct node *n)
         temp = n->next;
     }
 
-    struct node_and_int *pair = malloc_node_and_int();
+    struct node_and_int *pair = malloc__node_and_int();
     pair->node = temp;
     pair->data = n->data;
 
-    free_node(n);       
+    free__node(n);       
     return pair;
 }

src/examples/Dbl_Linked_List/remove_orig.broken.c

@@ -15,10 +15,10 @@ struct node_and_int *remove(struct node *n)
         temp = n->next;
     }
 
-    struct node_and_int *pair = malloc_node_and_int();
+    struct node_and_int *pair = malloc__node_and_int();
     pair->node = temp;
     pair->data = n->data;
 
-    free_node(n);       
+    free__node(n);       
     return pair;
 }

src/examples/Dbl_Linked_List/singleton.c

@@ -2,10 +2,10 @@
 
 struct node *singleton(int element)
 /*@ ensures take Ret = Dll_at(return);
-        Ret == Dll{left: Seq_Nil{}, curr: struct node{data: element, prev: NULL, next: NULL}, right: Seq_Nil{}};
+        Ret == Dll{left: Nil{}, curr: struct node{data: element, prev: NULL, next: NULL}, right: Nil{}};
 @*/
 {
-   struct node *n = malloc_node();
+   struct node *n = malloc__node();
    n->data = element;
    n->prev = 0;
    n->next = 0;

src/examples/abs.c

@@ -7,8 +7,7 @@ int abs (int x)
 {
   if (x >= 0) {
     return x;
-  }
-  else {
+  } else {
     return -x;
   }
 }

src/examples/abs_mem.c

@@ -2,8 +2,8 @@ int abs_mem (int *p)
 /* --BEGIN-- */
 /*@ requires take x = Owned<int>(p);
              MINi32() < x;
-    ensures take x2 = Owned<int>(p);
-            x == x2;
+    ensures take x_post = Owned<int>(p);
+            x == x_post;
             return == ((x >= 0i32) ? x : (0i32-x));
 @*/
 /* --END-- */

src/examples/add_0.c

@@ -1,7 +1,7 @@
 int add(int x, int y)
 /* --BEGIN-- */
-/*@ requires let sum = (i64) x + (i64) y;
-             -2147483648i64 <= sum; sum <= 2147483647i64; @*/
+/*@ requires let Sum = (i64) x + (i64) y;
+             -2147483648i64 <= Sum; Sum <= 2147483647i64; @*/
 /* --END-- */
 {
   return x+y;