Documentation followup on v0.1 release (#66)

README.md

@@ -1,7 +1,8 @@
 # Dusa Language
 
-Dusa is a logic programming language that has features of both Datalog and
-answer set programming.
+Dusa is an implementation of
+[finite-choice logic programming](https://arxiv.org/abs/2405.19040), which
+takes ideas from logic programming in both Datalog and answer set programming.
 
 [![Run static checks](https://github.com/robsimmons/dusa/actions/workflows/check.yml/badge.svg)](https://github.com/robsimmons/dusa/actions/workflows/check.yml)
 [![Coverage Status](https://coveralls.io/repos/github/robsimmons/dusa/badge.svg?branch=main)](https://coveralls.io/github/robsimmons/dusa?branch=main)

docs/src/content/docs/docs/language/choice.mdx

@@ -4,18 +4,20 @@ title: Choices
 
 import Dusa from '../../../../components/Dusa.astro';
 
-[Functional facts](functional-propositions) are a key part of how Dusa works: if a
-solution in Dusa contains a fact like `color 3 8 is "red"` then we know it can't 
-contain a fact like `color 3 8 is "black"`, because an attribute like `color 3 8` 
-is only allowed to "map" to at most one value.
+[Functional facts](/docs/language/facts/) are a key part of how Dusa works: if
+a solution in Dusa contains a fact like `color 3 8 is "red"` then we know it
+can't  contain a fact like `color 3 8 is "black"`, because an attribute like 
+`color 3 8`  is only allowed to "map" to at most one value.
 
-Dusa allows programmers to write programs with multiple solutions by saying that it's 
-possible to choose multiple attributes for a single value. Choices can be _open_ or _closed_. 
+Dusa allows programmers to write programs with multiple solutions by saying 
+that it's possible to choose multiple attributes for a single value. Choices 
+can be _open_ or _closed_. 
 
 ## Closed choices
 
-A closed choice lists an attribute, the keyword `is` and one or more values: if there
-is more than one value, the values are surrounded by curly braces and separated by commas.
+A closed choice lists an attribute, the keyword `is` and one or more values: 
+if there is more than one value, the values are surrounded by curly braces and
+separated by commas.
 
 In any solution,
 the attribute _must_ have one of the listed values.
@@ -30,11 +32,12 @@ color 3 8 is { "black", "red" }.
 
 [Explore this example on dusa.rocks](https://dusa.rocks/#jsonz=jcqxCoMwFIXhVzkcVxG0HcTV17iLJhdaGnMl0Uny7mLBtXT7-fkObhxoq0bW9Ob2ReN1KozBsnqkPWiGe5llxQRnwZJEid9AiyfeGQeEc5jcR1hDmNQLUZpbdWj_UA_0PxTLCQ)
 
-These three closed rules mean that the program has 2 to the power of 3 solutions. 
+These three closed rules mean that the program has 2 to the power of 3
+solutions. 
 
-Whenever we write a simple fact about a functional proposition in a program, like 
-`color 4 7 is "red"`, that's actually describing a closed rule with just one choice:
-we could equivalently write `color 4 7 is { "red" }`.
+Whenever we write a simple fact about a functional proposition in a program, 
+like `color 4 7 is "red"`, that's actually describing a closed rule with just 
+one choice: we could equivalently write `color 4 7 is { "red" }`.
 
 ### Closed choices describe intersections
 
@@ -48,31 +51,34 @@ a is { "blue", "orange", "green" }.
 
 `}/>
 
-The rules of forward chaining logic programming say that every rule that can fire must
-fire, and this program has two rules that can fire. If we imagine considering the first
-choice first, there are three potential solutions: the first just
-contains `a is "blue"`, the second just contains `a is "orange"`, and the third just
-contains `a is "red"`.
+The rules of forward chaining logic programming say that every rule that can 
+fire must fire, and this program has two rules that can fire. If we imagine 
+considering the first choice first, there are three potential solutions: the 
+first just contains `a is "blue"`, the second just contains `a is "orange"`, 
+and the third just contains `a is "red"`.
 
-- In the first potential solution, where `a is "blue"`, there's only one valid option for the second
-  choice: choosing blue. Choosing orange or green will just invalidate the
-  potential solution. 
-- Analogously, in the second potential solution where `a is "orange"`, there's only one valid way
-  to make the second choice.
-- In the third potential solution, where `a is "red"`, there's no way to make a consistent choice,
-  so this potential solution must be invalidated.
+- In the first potential solution, where `a is "blue"`, there's only one valid 
+  option for the second choice: choosing blue. Choosing orange or green will 
+  just invalidate the potential solution. 
+- Analogously, in the second potential solution where `a is "orange"`, there's
+  only one valid way to make the second choice.
+- In the third potential solution, where `a is "red"`, there's no way to make 
+  a consistent choice, so this potential solution must be invalidated.
 
 ## Open choices
 
-An open choice lists an attribute the keyword `is?`, and one or more values: if there
-is more than one value, the values are surrounded by curly braces and separated by commas.
+An open choice lists an attribute the keyword `is?`, and one or more values: 
+if there is more than one value, the values are surrounded by curly braces and
+separated by commas.
 
-In any solution, the attribute _must_ have some value, and that attribute _can_ be any 
-of the listed values... but it doesn't have to be! Open choices are very chill.
+In any solution, the attribute _must_ have some value, and that attribute 
+_can_ be any of the listed values... but it doesn't have to be! Open choices
+are very chill.
 
 ### Open rules describe unions
 
-The following programs all have exactly 3 solutions: `a is 1`, `a is 2`, and `a is 3`.
+The following programs all have exactly 3 solutions: `a is 1`, `a is 2`, and 
+`a is 3`.
 
 **Program 1**
 
@@ -102,6 +108,6 @@ a is? { 2, 3 }.
 `}/>
 
 Because open choices don't preclude other consistent assignments, the possible
-assignments are the union of the different assignments proposed by different open
-rules.
+assignments are the union of the different assignments proposed by different
+open rules.
 

docs/src/content/docs/docs/language/syntax.md

@@ -45,7 +45,5 @@ treated like whitespace.
                        |  <builtin-identifier> <arguments>
     <builtin>         ::= "BOOLEAN_TRUE" | "BOOLEAN_FALSE"
                        |  "NAT_ZERO" | "NAT_SUCC"
-                       |  "INT_PLUS" | "INT_MINUS" | "INT_TIMES
+                       |  "INT_PLUS" | "INT_MINUS" | "INT_TIMES"
                        |  "STRING_CONCAT"
-                       |  "CHECK_GT" | "CHECK_GEQ"
-                       |  "CHECK_LT" | "CHECK_LEQ"