From afb9d627f5bfdbea2d90f4eccc5653f763e51cc1 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Fri, 8 Jun 2018 13:21:29 +0200 Subject: [PATCH] convert Naming to markdown --- Naming.md | 84 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ README.md | 3 +- naming.txt | 79 -------------------------------------------------- 3 files changed, 86 insertions(+), 80 deletions(-) create mode 100644 Naming.md delete mode 100644 naming.txt diff --git a/Naming.md b/Naming.md new file mode 100644 index 000000000..7df509027 --- /dev/null +++ b/Naming.md @@ -0,0 +1,84 @@ +# Naming conventions for variables/arguments/hypotheses in the Coq development + +## small letters + +* a : A = cmraT or cofeT +* b : B = cmraT or cofeT +* c +* d +* e : expr = expressions +* f = some generic function +* g = some generic function +* h : heap +* i +* j +* k +* l +* m : iGst = ghost state +* n +* o +* p +* q +* r : iRes = resources +* s = state (STSs) +* s = stuckness bits +* t +* u +* v : val = values of language +* w +* x +* y +* z + +## capital letters + +* A : Type, cmraT or cofeT +* B : Type, cmraT or cofeT +* C +* D +* E : coPset = Viewshift masks +* F = a functor +* G +* H = hypotheses +* I = indexing sets +* J +* K : ectx = evaluation contexts +* K = keys of a map +* L +* M = maps / global CMRA +* N : namespace +* O +* P : uPred, iProp or Prop +* Q : uPred, iProp or Prop +* R : uPred, iProp or Prop +* S : set state = state sets in STSs +* T : set token = token sets in STSs +* U +* V : abstraction of value type in frame shift assertions +* W +* X : sets +* Y : sets +* Z : sets + +## small greek letters + +* γ : gname +* σ : state = state of language +* φ : interpretation of STS/Auth + +## capital greek letters + +* Φ : general predicate (over uPred, iProp or Prop) +* Ψ : general predicate (over uPred, iProp or Prop) + +# Naming conventions for algebraic classes in the Coq development + +## Suffixes + +* T: canonical structurs (for example ofeT for OFEs, cmraT for cameras) + +* C: OFEs +* R: cameras +* UR: unital cameras or resources algebras +* F: functors (can be combined with all of the above, e.g. CF is an OFE functor) +* G: global camera functor management diff --git a/README.md b/README.md index 92708d0fc..9e2d1e325 100644 --- a/README.md +++ b/README.md @@ -81,7 +81,8 @@ followed by `make build-dep`. document is [available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf). * Information on how to set up your editor for unicode input and output is collected in [Editor.md](Editor.md). -* The Iris Proof Mode (IPM) is documented at [ProofMode.md](ProofMode.md) +* The Iris Proof Mode (IPM) is documented at [ProofMode.md](ProofMode.md). +* Naming conventions are documented at [Naming.md](Naming.md). ## Case Studies diff --git a/naming.txt b/naming.txt deleted file mode 100644 index 5fd181827..000000000 --- a/naming.txt +++ /dev/null @@ -1,79 +0,0 @@ ------------------- Naming conventions for variables/arguments/hypotheses in the Coq development ------------------ - -== small letters == -a : A : cmraT or cofeT -b : B : cmraT or cofeT -c -d -e : expr = expressions -f : some generic function -g : some generic function -h : heap -i -j -k -l -m : iGst = ghost state -n -o -p -q -r : iRes = resources -s : state (STSs), stuckness bits -t -u -v : val = values of language -w -x -y -z - -== capital letters == -A : Type, cmraT or cofeT -B : Type, cmraT or cofeT -C -D -E : coPset = Viewshift masks -F : a functor -G -H : hypotheses -I : indexing sets -J -K : ectx = evaluation contexts - keys of a map -L -M : maps / global CMRA -N : namespace -O -P : uPred, iProp or Prop -Q : uPred, iProp or Prop -R : uPred, iProp or Prop -S : set state = state sets in STSs -T : set token = token sets in STSs -U -V : abstraction of value type in frame shift assertions -W -X : sets -Y : sets -Z : sets - -== small greek letters == -γ : gname -σ : state = state of language -φ : interpretation of STS/Auth - -== capital greek letters == -Φ : general predicate (over uPred, iProp or Prop) -Ψ : general predicate (over uPred, iProp or Prop) - ------------------- Naming conventions for algebraic classes in the Coq development ------------------ - -== Suffixes == - -T: canonical structurs (for example ofeT for OFEs, cmraT for cameras) - -C: OFEs -R: cameras -UR: unital cameras or resources algebras -F: functors (can be combined with all of the above, e.g. CF is an OFE functor) -G: global camera functor management -- GitLab