rename clause keyword to relation

TODO.md

@@ -1,3 +1,5 @@
+用 constraint programming 的知识来实现类型检查器。
+
 `Data` instead of `Term` -- only defined by `datatype`
 
 [maybe] remove eval

docs/books/clause-and-effect/01-party-pairs.ch → docs/examples/books/clause-and-effect/01-party-pairs.ch

@@ -1,10 +1,10 @@
-clause Male({ name: "bertram" })
-clause Male({ name: "percival" })
+relation Male({ name: "bertram" })
+relation Male({ name: "percival" })
 
-clause Female({ name: "lucinda" })
-clause Female({ name: "camilla" })
+relation Female({ name: "lucinda" })
+relation Female({ name: "camilla" })
 
-clause Pair({ male, female }) -- {
+relation Pair({ male, female }) -- {
   Male({ name: male })
   Female({ name: female })
 }

docs/books/clause-and-effect/02-drinking-pairs.ch → docs/examples/books/clause-and-effect/02-drinking-pairs.ch

@@ -1,11 +1,11 @@
-clause Drink({ person: "john", alcohol: "martini" })
-clause Drink({ person: "mary", alcohol: "gin" })
-clause Drink({ person: "susan", alcohol: "vodka" })
-clause Drink({ person: "john", alcohol: "gin" })
-clause Drink({ person: "fred", alcohol: "gin" })
-clause Drink({ person: "fred", alcohol: "vodka" })
+relation Drink({ person: "john", alcohol: "martini" })
+relation Drink({ person: "mary", alcohol: "gin" })
+relation Drink({ person: "susan", alcohol: "vodka" })
+relation Drink({ person: "john", alcohol: "gin" })
+relation Drink({ person: "fred", alcohol: "gin" })
+relation Drink({ person: "fred", alcohol: "vodka" })
 
-clause Friendship({ left, right, alcohol })
+relation Friendship({ left, right, alcohol })
 ------------------------------------ {
   Drink({ person: left, alcohol })
   Drink({ person: right, alcohol })

docs/examples/books/clause-and-effect/03-affordable-journeys.ch

@@ -0,0 +1,37 @@
+relation Border("sussex", "kent")
+relation Border("sussex", "surrey")
+relation Border("surrey", "kent")
+relation Border("hampshire", "sussex")
+relation Border("hampshire", "surrey")
+relation Border("hampshire", "berkshire")
+relation Border("berkshire", "surrey")
+relation Border("wiltshire", "hampshire")
+relation Border("wiltshire", "berkshire")
+
+relation Adjacent(x, y)
+---------------- border {
+  Border(x, y)
+}
+
+relation Adjacent(x, y)
+---------------- symmetry {
+  Border(y, x)
+}
+
+relation Affordable(x, y)
+-------------------- {
+  Adjacent(x, z)
+  Adjacent(z, y)
+}
+
+print find to_kent {
+  Affordable(to_kent, "kent")
+}
+
+print find to_sussex {
+  Affordable("sussex", to_sussex)
+}
+
+print find [x, y] {
+  Affordable(x, y)
+}

docs/examples/books/clause-and-effect/04-acyclic-directed-graph.ch

@@ -0,0 +1,31 @@
+relation Edge("g", "h")
+relation Edge("g", "d")
+relation Edge("e", "d")
+relation Edge("h", "f")
+relation Edge("e", "f")
+relation Edge("a", "e")
+relation Edge("a", "b")
+relation Edge("b", "f")
+relation Edge("b", "c")
+relation Edge("f", "c")
+
+relation Path(x, x)
+------------ {}
+
+relation Path(x, y)
+------------ {
+  Edge(x, z)
+  Path(z, y)
+}
+
+print find x {
+  Path("g", x)
+}
+
+print find x {
+  Path(x, "h")
+}
+
+print find [x, y] {
+  Path(x, y)
+}

docs/books/clause-and-effect/05-member.ch → docs/examples/books/clause-and-effect/05-member.ch

@@ -1,7 +1,7 @@
-clause Member(element, [element | _tail])
+relation Member(element, [element | _tail])
 ------------------------------------ here {}
 
-clause Member(element, [_head | tail])
+relation Member(element, [_head | tail])
 --------------------------------- there {
   Member(element, tail)
 }

docs/books/clause-and-effect/06-length-of-a-list.ch → docs/examples/books/clause-and-effect/06-length-of-a-list.ch

@@ -1,11 +1,11 @@
 import { Zero, Add1, One, Two } from "../../std/nat/index.ch"
 
-clause Length([], n)
+relation Length([], n)
 -------------------- {
   Zero(n)
 }
 
-clause Length([_head | tail], n)
+relation Length([_head | tail], n)
 -------------------------------- {
   Add1(prev, n)
   Length(tail, prev)

docs/books/clause-and-effect/08-maximum-of-a-list.ch → docs/examples/books/clause-and-effect/08-maximum-of-a-list.ch

@@ -1,13 +1,13 @@
-// clause Max(null, n, n)
+// relation Max(null, n, n)
 // ---------------- {}
 
-// clause Max(cons(x, rest), n, max)
+// relation Max(cons(x, rest), n, max)
 // ---------------------------- {
 //   Max(rest, x, max)
 //   x > n
 // }
 
-// clause Max(cons (x, rest), n, max)
+// relation Max(cons (x, rest), n, max)
 // ---------------------------- {
 //   Max(rest, n, max)
 //   x <= n

docs/books/clause-and-effect/09-searching-a-cyclic-graph.ch → docs/examples/books/clause-and-effect/09-searching-a-cyclic-graph.ch

@@ -1,30 +1,30 @@
-clause Edge("g", "h")
-clause Edge("d", "a")
-clause Edge("g", "d")
-clause Edge("e", "d")
-clause Edge("h", "f")
-clause Edge("e", "f")
-clause Edge("a", "e")
-clause Edge("a", "b")
-clause Edge("b", "f")
-clause Edge("b", "c")
-clause Edge("f", "c")
+relation Edge("g", "h")
+relation Edge("d", "a")
+relation Edge("g", "d")
+relation Edge("e", "d")
+relation Edge("h", "f")
+relation Edge("e", "f")
+relation Edge("a", "e")
+relation Edge("a", "b")
+relation Edge("b", "f")
+relation Edge("b", "c")
+relation Edge("f", "c")
 
 // "a", "e", "d" -- in a loop
 
 // We define `Legal` to rule out loop -- to avoid searching in a loop
 
-clause Legal(_, [])
+relation Legal(_, [])
 
-clause Legal(z, [head | tail])
+relation Legal(z, [head | tail])
 ---------------------------- {
   NotEqual(z, head)
   Legal(z, tail)
 }
 
-clause Path(x, x, _occurs)
+relation Path(x, x, _occurs)
 
-clause Path(x, y, occurs)
+relation Path(x, y, occurs)
 ------------------------ {
   Edge(x, z)
   Legal(z, occurs)