1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
(datatype List
(Nil)
(Cons i64 List))
(ruleset list-ruleset)
(function list-length (List) i64 :no-merge)
(relation list-length-demand (List))
(rule
((list-length-demand (Nil)))
((set (list-length (Nil)) 0))
:ruleset list-ruleset)
(rule
((list-length-demand (Cons head tail)))
((list-length-demand tail))
:ruleset list-ruleset)
(rule
( (list-length-demand (Cons head tail))
(= (list-length tail) tail-length))
((set (list-length (Cons head tail)) (+ tail-length 1)))
:ruleset list-ruleset)
(function list-get (List i64) i64 :no-merge)
(relation list-get-demand (List i64))
(rule
( (list-get-demand list 0)
(= list (Cons head tail)))
((set (list-get list 0) head))
:ruleset list-ruleset)
(rule
( (list-get-demand list n) (> n 0)
(= list (Cons head tail)))
((list-get-demand tail (- n 1)))
:ruleset list-ruleset)
(rule
( (list-get-demand list n)
(= list (Cons head tail))
(= item (list-get tail (- n 1))))
((set (list-get list n) item))
:ruleset list-ruleset)
(constructor list-append (List List) List)
(rewrite (list-append (Nil) list) list :ruleset list-ruleset)
(rewrite (list-append (Cons head tail) list) (Cons head (list-append tail list)) :ruleset list-ruleset)
; list-contains Nil _ => false
; list-contains (Cons item tail) item => true
; list-contains (Cons head tail) item => assert(head != item); (list-contains tail item)
; list-contains needs inequality
(constructor list-set (List i64 i64) List)
(rewrite (list-set (Cons head tail) 0 item) (Cons item tail) :ruleset list-ruleset)
(rewrite (list-set (Cons head tail) i item) (Cons head (list-set tail (- i 1) item)) :when ((> i 0)) :ruleset list-ruleset)
; Tests
(let $a (Cons 1 (Cons 2 (Nil))))
(let $b (Cons 3 (Nil)))
(let $c (Cons 1 (Cons 2 (Cons 3 (Nil)))))
(let $d (Cons 1 (Cons 4 (Nil))))
(let $e (list-append $a $b))
(let $f (list-set $a 1 4))
(list-length-demand $c)
(list-get-demand $b 0)
(list-get-demand $a 1)
(run-schedule (saturate (run list-ruleset)))
(check (= $e $c))
(check (= (list-length $c) 3))
(check (= (list-get $b 0) 3))
(check (= (list-get $a 1) 2))
(check (= $f $d))