Update language reference to match current state of Juvix (#1594)

* docs: ℕ to Nat

* docs: Add emacs goto definition

* Document juvix-format-buffer and add emacs keybinding

* docs: replace ghc with c in compile block examples

* Update CLI documentation

* doc: replace ↦ and → with ->

docs/org/language-reference/compile-blocks.org

@@ -3,7 +3,7 @@
 The compile keyword has two arguments:
 
 - A name of an expression to be compiled.
-- A set of compilation rules using the format (=backend= → =string=)
+- A set of compilation rules using the format (=backend= -> =string=)
   where the string is the text we inline.
 
 This is an example:
@@ -13,7 +13,7 @@ $ cat tests/positive/HelloWorld
 ...
 axiom Action : Type;
 compile Action {
- ghc ↦ "IO ()";
+  c -> "int";
 };
 ...
 #+end_src
@@ -26,8 +26,8 @@ The following Juvix examples are NOT valid.
 ...
 axiom Action : Type;
 compile Action {
- ghc ↦ "IO ()";
- ghc ↦ "IO ()";  --
+ c -> "int";
+ c -> "int";  --
 };
 ...
 #+end_src
@@ -38,10 +38,10 @@ compile Action {
 ...
 axiom Action : Type;
 compile Action {
- ghc ↦ "IO ()";
+ c -> "int";
 };
 compile Action {
- ghc ↦ "IO ()";
+ c -> "int";
 };
 ...
 #+end_src
@@ -59,7 +59,7 @@ axiom Action : Type;
 $ cat B.mjuvix
 ...
 compile Action {
- ghc ↦ "IO ()";
+ c -> "int";
 };
 ...
 #+end_src

docs/org/language-reference/foreign-blocks.org

@@ -11,7 +11,7 @@ The following is an example taken from the Juvix standard library.
 module Integers;
 
 axiom Int : Type;
-compile Int {  c ↦ "int" };
+compile Int {  c -> "int" };
 
 foreign c {
    bool lessThan(int l, int r) {
@@ -25,12 +25,12 @@ inductive Bool {
 };
 
 infix 4 <';
-axiom <' : Int → Int → Bool;
+axiom <' : Int -> Int -> Bool;
 compile <' {
-  c ↦ "lessThan";
+  c -> "lessThan";
 };
 
 infix 4 <;
-< : Int → Int → Bool;
+< : Int -> Int -> Bool;
 < a b := from-backend-bool (a <' b);
 #+end_example

docs/org/language-reference/functions.org

@@ -4,13 +4,13 @@ A function declaration is a type signature /and/ a group of definitions called
 /function clauses/.
 
 In the following example we define a function called =multiplyByTwo=. The first
-line =multiplyByTwo : ℕ -> ℕ;= is the type signature and the second line
+line =multiplyByTwo : Nat -> Nat;= is the type signature and the second line
 ~multiplyByTwo n := 2 * n;~ is a function clause.
 
 #+begin_example
 open import Stdlib.Prelude;
 
-multiplyByTwo : ℕ -> ℕ;
+multiplyByTwo : Nat -> Nat;
 multiplyByTwo n := 2 * n;
 #+end_example
 

docs/org/language-reference/inductive-data-types.org

@@ -20,7 +20,7 @@ by =suc zero= or the number two represented by =suc (suc zero)=, etc.
 #+begin_example
 inductive Nat {
     zero : Nat;
-    suc : Nat → Nat;
+    suc : Nat -> Nat;
 };
 #+end_example
 
@@ -29,7 +29,7 @@ Let us define, for example, the function for adding two natural numbers.
 
 #+begin_src text
 inifl 6 +;
-+ : Nat → Nat → Nat;
++ : Nat -> Nat -> Nat;
 + zero b := b;
 + (suc a) b := suc (a + b);
 #+end_src
@@ -45,10 +45,10 @@ the following type taken from the Juvix standard library:
 infixr 5 ∷;
 inductive List (A : Type) {
   nil : List A;
-  ∷ : A → List A → List A;
+  ∷ : A -> List A -> List A;
 };
 
-elem : {A : Type} → (A → A → Bool) → A → List A → Bool;
+elem : {A : Type} -> (A -> A -> Bool) -> A -> List A -> Bool;
 elem _ _ nil := false;
 elem eq s (x ∷ xs) := eq s x || elem eq s xs;
 #+end_example

docs/org/tooling/CLI.org

@@ -3,7 +3,7 @@
 ** Usage
 
 #+begin_src shell
-juvix [Global options]  ((-v|--version) | --show-root | COMMAND)
+juvix [Global options] ((-v|--version) | (-h|--help) | COMPILER_CMD | UTILITY_CMD)
 #+end_src
 
 ** Informative options
@@ -26,18 +26,29 @@ juvix [Global options]  ((-v|--version) | --show-root | COMMAND)
 - =--only-errors=
   Only print errors in a uniform format (used by
                           juvix-mode)
+- =--no-termination=
+  Disable termination checking
+- =--no-positivity=
+  Disable positivity checking for inductive types
+- =--no-stdlib=
+  Do not use the standard library
 
 ** Main Commands
 
 - =html=
   Generate HTML output from a Juvix file
-
 - =typecheck=
   Typecheck a Juvix file
-
 - =compile=
   Compile a Juvix file
 
+** Utility Commands
+
+- =doctor=
+  Perform checks on your Juvix development environment
+- =init=
+  Interactively initialize a juvix project in the current directory
+
 ** Dev Commands
 
 #+begin_src shell
@@ -48,6 +59,16 @@ juvix dev COMMAND
   Parse a Juvix file
 - =scope=
   Parse and scope a Juvix file
+- =highlight=
+  Highlight a Juvix file
+- =core=
+  Subcommands related to JuvixCore
+- =asm=
+  Subcommands related to JuvixAsm
+- =doc=
+  Generate documentation
+- =root=
+  Show the root path for a Juvix project
 - =termination=
   Subcommands related to termination checking
 - =internal=

docs/org/tooling/emacs-mode.org

@@ -17,9 +17,11 @@ The Juvix major mode will be activated automatically for =.juvix= files.
 
 *** Keybindings
 
-  | Key       | Function Name    | Description                                           |
-  |-----------+------------------+-------------------------------------------------------|
-  | =C-c C-l= | =juvix-load= | Runs the scoper and adds semantic syntax highlighting |
+  | Key       | Function Name           | Description                                           |
+  |-----------+-------------------------+-------------------------------------------------------|
+  | =C-c C-l= | =juvix-load=            | Runs the scoper and adds semantic syntax highlighting |
+  | =M-.=     | =juvix-goto-definition= | Go to the definition of symbol at point               |
+  | =C-c C-f= | =juvix-format-buffer=   | Format the current buffer                             |
 
 *** Emacs installation
 

juvix-mode/juvix-mode.el

@@ -12,6 +12,7 @@
         (menu-map (make-sparse-keymap "Juvix")))
     (define-key map (kbd "C-c C-l") 'juvix-load)
     (define-key map (kbd "M-.") 'juvix-goto-definition)
+    (define-key map (kbd "C-c C-f") 'juvix-format-buffer)
     map)
   "Keymap for Juvix mode.")