Add more Mangle readthedocs documentation.

Rename golang package for the interactive interpreter to "mg"

PiperOrigin-RevId: 662960424

docs/spec_decls.md

@@ -94,15 +94,16 @@ A type expression is first-order if it does not contain function types or
 relation types. What follows is a description of type constants and functions
 that can be used to build first-order type expressions.
 
-The following type constants:
+The following type constants describe first-order types:
 
 *   `/any`
 *   `/number`
 *   `/float64`
 *   `/string`
+*   `/bytes`
 
-The following type-level functions, where all arguments are first-order type
-expressions:
+The following type-level functions describe first-order types, assuming that
+all arguments are first-order type expressions:
 
 *   `fn:List(T)` type of list
 *   `fn:Pair(S, T)` type of pairs

interpreter/main/main.go → interpreter/mg/mg.go

@@ -12,7 +12,7 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 
-// Binary shell is a shell for interactive interpreter.
+// Binary mg is a shell for the interactive interpreter.
 package main
 
 import (

readthedocs/README.md

@@ -3,3 +3,23 @@
 [![Documentation Status](https://readthedocs.org/projects/mangle/badge/?version=latest)](https://readthedocs.org/projects/mangle/builds/)
 
 This repository contains Mangle documentation sources. Rendered documentation is hosted on [mangle.readthedocs.io](http://mangle.readthedocs.io).
+
+## Setting up an environment
+
+```
+> python -m venv manglereadthedocs
+> . manglereadthedocs/bin/activate
+(manglereadthedocs) > pip install -U sphinx
+(manglereadthedocs) > READTHEDOCS=<path to readthedocs dir>
+(manglereadthedocs) > pip install -r ${READTHEDOCS}/requirements.txt
+```
+
+## Building the documentation
+
+```
+> . manglereadthedocs/bin/activate
+(manglereadthedocs) > READTHEDOCS=<path to readthedocs dir>
+(manglereadthedocs) > sphinx-build -M html ${READTHEDOCS} output
+```
+
+The output can be found in the `output/html` directory.

readthedocs/conf.py

@@ -16,5 +16,6 @@
 source_suffix = ['.md']
 extensions = ['myst_parser']
 
+html_theme = 'bizstyle'
 templates_path = ['_templates']
-exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']
+exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store', 'README.md']

readthedocs/datatypes.md

@@ -0,0 +1,90 @@
+# Data Types
+
+## Names
+
+Names are identifiers. They refer to some entity or object.
+
+Name can also be structured, in the sense that they can
+have several non-empty parts separated by `/`. They are similar to URLs
+but without the protocol.
+
+```
+/a
+/test12
+/antigone
+
+/crates.io/fnv
+/home.cern/news/news/computing/30-years-free-and-open-web
+```
+
+Two distinct names always refer to distinct objects ("unique name assumption").
+The objects they refer to are also always different from other constants,
+e.g. numbers, strings.
+
+## Integer Numbers
+
+The `/number` type stands for 64-bit signed integers.
+
+```
+0
+1
+128
+-10000
+```
+
+## Floating point Numbers
+
+The `/float64` type stands for 64-bit floating point numbers.
+
+```
+3.141592
+-10.5
+```
+
+## Strings
+
+The `/string` type stands for strings (sequences of characters).
+
+Strings can be written in single or double quotes.
+
+```
+"foo"
+'foo'
+"something 'quoted'"
+'something "quoted"'
+```
+
+Strings can contain escapes:
+
+```
+"something \"quoted\" with escapes."
+'A single quote \' surrounded by single quotes'
+"A single quote \' surrounded by double quotes"
+"A double quote \" surrounded by double quotes"
+"A newline \n"
+"A tab \t"
+"Java class files start with \xca\xfe\xba\xbe"
+"The \u{01f624} emoji was originally called 'Face with Look of Triumph'"
+```
+
+Multi-line strings are supported using backticks
+
+```
+`
+I write, erase, rewrite
+
+Erase again, and then
+
+A poppy blooms.
+`
+```
+
+## Byte strings
+
+The `/bytes` type stands for sequences of arbitrary bytes.
+
+Byte strings can still be written as literals.
+
+```
+b"A \x80 byte carries special meaning in UTF8 encoded strings"
+```

readthedocs/index.md

@@ -1,5 +1,54 @@
-Mangle is a logic programming language based on datalog.
+# Mangle Datalog
 
-It extends datalog with facilities like aggregation, function calls, static type-checking and type inference.
+Mangle Datalog is a logic programming language and deductive database system.
 
-Documentation is under construction. In the meantime, please see https://github.com/google/mangle for more information.
+It is declarative:
+users communicate to the system what they want, not a series of commands.
+
+Data is represented using *facts* and derived with *rules*. A fact combines
+several values into a statement, and a rule describes how to compute new
+facts from existing facts.
+
+Here is an example describing a family from a Greek tragedy, Antigone:
+
+```cplint
+parent(/oedipus, /antigone).
+parent(/oedipus, /ismene).
+parent(/oedipus, /eteocles).
+parent(/oedipus, /polynices).
+
+sibling(Person1, Person2) :-
+   parent(P, Person1), parent(P, Person2), Person1 != Person2.
+```
+
+The `sibling` rule declaration describes what a sibling is.
+We can now ask who Antigone's siblings are:
+
+```cplint
+mg >? sibling(/antigone, X)
+sibling(/antigone,/eteocles)
+sibling(/antigone,/ismene)
+sibling(/antigone,/polynices)
+Found 3 entries for sibling(/antigone,_).
+```
+
+Here `X` is a variable, `? sibling(/antigone, X)` is a query that is asking
+what are possible values of `X`.
+
+Mangle extends Datalog with facilities like aggregation, function calls,
+static type-checking and type inference.
+
+Documentation is under construction. In the meantime, please see the docs
+in the [documentation](https://github.com/google/mangle/blob/main/docs/README.md)
+and [examples directory](https://github.com/google/mangle/tree/main/examples)
+for more information.
+
+
+## Table of contents
+
+```{toctree}
+---
+maxdepth: 2
+---
+Installing <installing.md>
+Data Types <datatypes.md>

readthedocs/installing.md

@@ -0,0 +1,37 @@
+# Installing
+
+## Installing the go implementation
+
+You need to have Go programming language installed (see [instructions](https://go.dev/doc/install)).
+
+Assuming you want to install the interpreter to `~/bin/mg`, do the following:
+```
+GOBIN=~/bin go install github.com/google/mangle/interpreter/mg@latest
+```
+
+Then you can start the interpreter with `~/bin/mg`.
+
+## Building the go implementation from source
+
+```
+git clone github.com/google/mangle
+cd mangle
+go get -t ./...
+go build ./...
+go test ./...
+```
+
+You can start the interpreter using `go run interpreter/mg/mg.go`
+
+## Building the rust implementation from source
+
+```
+git clone github.com/google/mangle
+cd mangle/rust
+cargo build
+cargo test
+```
+
+```{note}
+The Rust implementation has no interactive interpreter yet.
+```