Revision of multiset-fib.modal

1

+

<> (tally ?v (Bag ?l)) ((Bag tallying| tallying> ?v ?l))

2

+

3

+

<> (tallying> ?v ())

4

+

(<tallying ((Entry ?v 1) ()))

5

+

6

+

<> (tallying> ?v ((Entry ?v ?c) ?r))

7

+

(<tallying ((Entry ?v ?((?: ?0 ?1) ?:) + ?c 1) ?r))

8

+

9

+

<> (tallying> ?v (?e ?r))

10

+

((?e tallying> ?v ?r))

11

+

12

+

<> ((Bag tallying| <tallying ?l)) ((Bag ?l))

13

+

<> ((?e <tallying ?p)) (<tallying (?e ?p))

14

+

15

+

<> (tally all ()) ()

16

+

<> (tally all (?i ?r) (Bag ?l)) (tally all ?r tally ?i (Bag ?l))

17

+

18

+

19

+

20

+

<> (find ?v (Bag ?l)) ((Bag find| find> ?v ?l))

21

+

22

+

<> (find> ?v ((Entry ?v ?c) ?r))

23

+

(<found #yes ((Entry ?v ?c) ?r))

24

+

<> (find> ?v ()) (<found #no ())

25

+

26

+

<> (find> ?v (?e ?r)) ((?e find> ?v ?r))

27

+

28

+

<> ((Bag find| <found ?a ?l)) (?a (Bag ?l))

29

+

<> ((?e <found ?a ?p)) (<found ?a (?e ?p))

30

+

31

+

32

+

33

+

<> (has all ()) (#yes)

34

+

<> (has all (?i ?r)) (?r has all| find ?i)

35

+

<> (?r has all| #yes) (has all ?r)

36

+

<> (?r has all| #no) (#no)

37

+

38

+

39

+

40

+

<> (remove ?i (Bag ?r)) ((Bag remove| remove> ?i ?r))

41

+

42

+

<> (remove> ?i ()) (<remove ())

43

+

<> (remove> ?i ((Entry ?i ?c) ?r)) (removing ((Entry ?i ?((?: ?0 ?1) ?:) - ?c 1) ?r))

44

+

<> (remove> ?i (?e ?r)) ((?e remove> ?i ?r))

45

+

46

+

<> (removing ((Entry ?i 0) ?r)) (<remove ?r)

47

+

<> (removing ((Entry ?i ?c) ?r)) (<remove ((Entry ?i ?c) ?r))

48

+

49

+

<> ((Bag remove| <remove ?l)) ((Bag ?l))

50

+

<> ((?e <remove ?p)) (<remove (?e ?p))

51

+

52

+

<> (remove all ()) ()

53

+

<> (remove all (?i ?r) (Bag ?l)) (remove all ?r remove ?i (Bag ?l))

54

+

55

+

56

+

<> (:) (takes>)

57

+

<> (takes> >) (g>)

58

+

<> (g> ;) ((Recipe () ()))

59

+

60

+

<> (takes> ?i) (take ?i takes>)

61

+

<> (g> ?i) (give ?i g>)

62

+

63

+

<> (give ?i (Recipe ?n ?g)) ((Recipe ?n (?i ?g)))

64

+

<> (take ?i (Recipe ?n ?g)) ((Recipe (?i ?n) ?g))

65

+

66

+

<> ((Recipe () ?g)) ()

67

+

68

+

<> (recipes) (recipes>)

69

+

70

+

<> (recipes> (Bag ?l)) (<ready (Bag ?l))

71

+

<> (recipes> (Recipe ?n ?g)) ((Recipe ?n ?g) recipes>)

72

+

73

+

<> ((Recipe ?n ?g) <ready) (<ready (Recipe ?n ?g))

74

+

<> (<ready) (rewrite)

75

+

76

+

<> (bag {) (bag)

77

+

<> (bag }) ((Bag ()))

78

+

<> (bag ?i) (tally ?i bag)

79

+

80

+

81

+

<> (rewrite (Recipe ?n ?g)) (rewrite| (Recipe ?n ?g) test> ?n)

82

+

83

+

<> (test> ?n (Bag ?l)) (test| ?n has all ?n (Bag ?l))

84

+

<> (test> ?n ?r) (?r test> ?n)

85

+

86

+

<> (test| ?n #yes) (match| #yes remove all ?n)

87

+

<> (test| ?n #no) (<match #no)

88

+

89

+

<> (match| #yes (Bag ?l)) (<match #yes (Bag ?l))

90

+

91

+

<> (rewrite| <match #yes (Recipe ?n ?g)) (rewrite| (Recipe ?n ?g) update> ?g)

92

+

<> (rewrite| <match #no) (rewrite>)

93

+

<> (?r <match ?a) (<match ?a ?r)

94

+

95

+

<> (update> ?g (Bag ?l)) (update| tally all ?g (Bag ?l))

96

+

<> (update> ?g ?r) (?r update> ?g)

97

+

98

+

<> (update| (Bag ?l)) (<update (Bag ?l))

99

+

100

+

<> (rewrite| <update) (<rewrite)

101

+

<> (?r <update) (<update ?r)

102

+

103

+

<> (?r <rewrite) (<rewrite ?r)

104

+

<> (<rewrite) (rewrite)

105

+

106

+

<> (rewrite (Bag ?l)) (done (Bag ?l))

107

+

<> (rewrite> ?r) (?r rewrite)

108

+

109

+

<> (?r done) (done)

110

+

111

+

112

+

recipes

113

+

: fib n > fib.shift ;

114

+

115

+

: fib.shift n1 > fib.shift N2 ;

116

+

: fib.shift n2 > fib.shift N1 N2 ;

117

+

: fib.shift > fib.move ;

118

+

119

+

: fib.move N1 > fib.move n1 ;

120

+

: fib.move N2 > fib.move n2 ;

121

+

: fib.move > fib ;

122

+

123

+

: n1 > ;

124

+

: fib > ;

125

+

126

+

127

+

bag { n n n n n n1 n2 fib }

capitalex / multiset-fib.modal

capitalex revised this gist 6 months ago. Go to revision

		@@ -0,0 +1,127 @@
1	+	<> (tally ?v (Bag ?l)) ((Bag tallying\| tallying> ?v ?l))
2	+
3	+	<> (tallying> ?v ())
4	+	(<tallying ((Entry ?v 1) ()))
5	+
6	+	<> (tallying> ?v ((Entry ?v ?c) ?r))
7	+	(<tallying ((Entry ?v ?((?: ?0 ?1) ?:) + ?c 1) ?r))
8	+
9	+	<> (tallying> ?v (?e ?r))
10	+	((?e tallying> ?v ?r))
11	+
12	+	<> ((Bag tallying\| <tallying ?l)) ((Bag ?l))
13	+	<> ((?e <tallying ?p)) (<tallying (?e ?p))
14	+
15	+	<> (tally all ()) ()
16	+	<> (tally all (?i ?r) (Bag ?l)) (tally all ?r tally ?i (Bag ?l))
17	+
18	+
19	+
20	+	<> (find ?v (Bag ?l)) ((Bag find\| find> ?v ?l))
21	+
22	+	<> (find> ?v ((Entry ?v ?c) ?r))
23	+	(<found #yes ((Entry ?v ?c) ?r))
24	+	<> (find> ?v ()) (<found #no ())
25	+
26	+	<> (find> ?v (?e ?r)) ((?e find> ?v ?r))
27	+
28	+	<> ((Bag find\| <found ?a ?l)) (?a (Bag ?l))
29	+	<> ((?e <found ?a ?p)) (<found ?a (?e ?p))
30	+
31	+
32	+
33	+	<> (has all ()) (#yes)
34	+	<> (has all (?i ?r)) (?r has all\| find ?i)
35	+	<> (?r has all\| #yes) (has all ?r)
36	+	<> (?r has all\| #no) (#no)
37	+
38	+
39	+
40	+	<> (remove ?i (Bag ?r)) ((Bag remove\| remove> ?i ?r))
41	+
42	+	<> (remove> ?i ()) (<remove ())
43	+	<> (remove> ?i ((Entry ?i ?c) ?r)) (removing ((Entry ?i ?((?: ?0 ?1) ?:) - ?c 1) ?r))
44	+	<> (remove> ?i (?e ?r)) ((?e remove> ?i ?r))
45	+
46	+	<> (removing ((Entry ?i 0) ?r)) (<remove ?r)
47	+	<> (removing ((Entry ?i ?c) ?r)) (<remove ((Entry ?i ?c) ?r))
48	+
49	+	<> ((Bag remove\| <remove ?l)) ((Bag ?l))
50	+	<> ((?e <remove ?p)) (<remove (?e ?p))
51	+
52	+	<> (remove all ()) ()
53	+	<> (remove all (?i ?r) (Bag ?l)) (remove all ?r remove ?i (Bag ?l))
54	+
55	+
56	+	<> (:) (takes>)
57	+	<> (takes> >) (g>)
58	+	<> (g> ;) ((Recipe () ()))
59	+
60	+	<> (takes> ?i) (take ?i takes>)
61	+	<> (g> ?i) (give ?i g>)
62	+
63	+	<> (give ?i (Recipe ?n ?g)) ((Recipe ?n (?i ?g)))
64	+	<> (take ?i (Recipe ?n ?g)) ((Recipe (?i ?n) ?g))
65	+
66	+	<> ((Recipe () ?g)) ()
67	+
68	+	<> (recipes) (recipes>)
69	+
70	+	<> (recipes> (Bag ?l)) (<ready (Bag ?l))
71	+	<> (recipes> (Recipe ?n ?g)) ((Recipe ?n ?g) recipes>)
72	+
73	+	<> ((Recipe ?n ?g) <ready) (<ready (Recipe ?n ?g))
74	+	<> (<ready) (rewrite)
75	+
76	+	<> (bag {) (bag)
77	+	<> (bag }) ((Bag ()))
78	+	<> (bag ?i) (tally ?i bag)
79	+
80	+
81	+	<> (rewrite (Recipe ?n ?g)) (rewrite\| (Recipe ?n ?g) test> ?n)
82	+
83	+	<> (test> ?n (Bag ?l)) (test\| ?n has all ?n (Bag ?l))
84	+	<> (test> ?n ?r) (?r test> ?n)
85	+
86	+	<> (test\| ?n #yes) (match\| #yes remove all ?n)
87	+	<> (test\| ?n #no) (<match #no)
88	+
89	+	<> (match\| #yes (Bag ?l)) (<match #yes (Bag ?l))
90	+
91	+	<> (rewrite\| <match #yes (Recipe ?n ?g)) (rewrite\| (Recipe ?n ?g) update> ?g)
92	+	<> (rewrite\| <match #no) (rewrite>)
93	+	<> (?r <match ?a) (<match ?a ?r)
94	+
95	+	<> (update> ?g (Bag ?l)) (update\| tally all ?g (Bag ?l))
96	+	<> (update> ?g ?r) (?r update> ?g)
97	+
98	+	<> (update\| (Bag ?l)) (<update (Bag ?l))
99	+
100	+	<> (rewrite\| <update) (<rewrite)
101	+	<> (?r <update) (<update ?r)
102	+
103	+	<> (?r <rewrite) (<rewrite ?r)
104	+	<> (<rewrite) (rewrite)
105	+
106	+	<> (rewrite (Bag ?l)) (done (Bag ?l))
107	+	<> (rewrite> ?r) (?r rewrite)
108	+
109	+	<> (?r done) (done)
110	+
111	+
112	+	recipes
113	+	: fib n > fib.shift ;
114	+
115	+	: fib.shift n1 > fib.shift N2 ;
116	+	: fib.shift n2 > fib.shift N1 N2 ;
117	+	: fib.shift > fib.move ;
118	+
119	+	: fib.move N1 > fib.move n1 ;
120	+	: fib.move N2 > fib.move n2 ;
121	+	: fib.move > fib ;
122	+
123	+	: n1 > ;
124	+	: fib > ;
125	+
126	+
127	+	bag { n n n n n n1 n2 fib }