Factor out lang/check/axioms.md
diff --git a/lang/check/axioms.md b/lang/check/axioms.md
new file mode 100644
index 0000000..af46e8d
--- /dev/null
+++ b/lang/check/axioms.md
@@ -0,0 +1,52 @@
+# Axioms
+
+This file lists Wuffs' axioms: a fixed list of built-in, self-evident rules to
+combine existing facts to create new facts. For example, given numerical-typed
+expressions `a`, `b` and `c`, the two facts that `a < c` and `c <= b` together
+imply that `a < b`: less-than-ness is transitive.
+
+Wuffs code represents this axiom by the string `"a < b: a < c; c <= b"`, and it
+is invoked by the `assert` and `via` keywords, naming the rule and [binding the
+expressions `a`, `b` and
+`c`](https://github.com/google/wuffs/blob/4080840928c0b05a80cda0d14ac2e2615f679f1a/std/lzw/decode_lzw.wuffs#L99).
+
+This file is not just documentation. It is
+[parsed](https://github.com/google/wuffs/blob/master/lang/check/gen.go) to give
+the list of axioms built into the Wuffs compiler.
+
+---
+
+- `"a < b: b > a"`
+- `"a < b: a < c; c < b"`
+- `"a < b: a < c; c == b"`
+- `"a < b: a == c; c < b"`
+- `"a < b: a < c; c <= b"`
+- `"a < b: a <= c; c < b"`
+
+---
+
+- `"a > b: b < a"`
+
+---
+
+- `"a <= b: b >= a"`
+- `"a <= b: a <= c; c <= b"`
+- `"a <= b: a <= c; c == b"`
+- `"a <= b: a == c; c <= b"`
+
+---
+
+- `"a >= b: b <= a"`
+
+---
+
+- `"a < (b + c): a < c; 0 <= b"`
+- `"a < (b + c): a < (b0 + c0); b0 <= b; c0 <= c"`
+
+---
+
+- `"a <= (a + b): 0 <= b"`
+
+---
+
+- `"(a + b) <= c: a <= (c - b)"`
diff --git a/lang/check/gen.go b/lang/check/gen.go
index bf8a28c..712f9ac 100644
--- a/lang/check/gen.go
+++ b/lang/check/gen.go
@@ -30,31 +30,6 @@
"strings"
)
-var reasons = [...]string{
- "a < b: b > a",
- "a < b: a < c; c < b",
- "a < b: a < c; c == b",
- "a < b: a == c; c < b",
- "a < b: a < c; c <= b",
- "a < b: a <= c; c < b",
-
- "a > b: b < a",
-
- "a <= b: b >= a",
- "a <= b: a <= c; c <= b",
- "a <= b: a <= c; c == b",
- "a <= b: a == c; c <= b",
-
- "a >= b: b <= a",
-
- "a < (b + c): a < c; 0 <= b",
- "a < (b + c): a < (b0 + c0); b0 <= b; c0 <= c",
-
- "a <= (a + b): 0 <= b",
-
- "(a + b) <= c: a <= (c - b)",
-}
-
func main() {
if err := main1(); err != nil {
os.Stderr.WriteString(err.Error() + "\n")
@@ -64,6 +39,10 @@
func main1() error {
out.WriteString(header)
+ reasons, err := loadReasons()
+ if err != nil {
+ return err
+ }
for _, reason := range reasons {
nextTmp = 0
names = map[string]bool{}
@@ -80,6 +59,36 @@
return ioutil.WriteFile("data.go", formatted, 0644)
}
+func loadReasons() ([]string, error) {
+ s, err := ioutil.ReadFile("axioms.md")
+ if err != nil {
+ return nil, err
+ }
+ dashes := []byte("\n\n---\n\n")
+ if i := bytes.Index(s, dashes); i < 0 {
+ return nil, fmt.Errorf("could not parse axioms.md")
+ } else {
+ s = s[i+len(dashes):]
+ }
+ ret := []string(nil)
+ lquotes := []byte("`\"")
+ rquotes := []byte("\"`")
+ for {
+ if i := bytes.Index(s, lquotes); i < 0 {
+ break
+ } else {
+ s = s[i+len(lquotes):]
+ }
+ if i := bytes.Index(s, rquotes); i < 0 {
+ break
+ } else {
+ ret = append(ret, string(s[:i]))
+ s = s[i+len(rquotes):]
+ }
+ }
+ return ret, nil
+}
+
var (
nextTmp int
names map[string]bool
