-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathprog.casl
162 lines (141 loc) · 4.53 KB
/
prog.casl
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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
%% This gives 24 stable models with 0 non-optimal steps
from Basic/StructuredDatatypes get List
from Basic/Numbers get Nat
spec SemSys =
sort PriorityDummySort
op prioDummyOp : PriorityDummySort
end
spec Symbols = SemSys then
generated type Note ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | x | x1
op __+__ : Note * Note -> Note
op suc : Note -> Note
. suc(0) = 1 %(AxSucc0:p:100:r:0)%
. suc(1) = 2 %(AxSucc1:p:100:r:0)%
. suc(2) = 3 %(AxSucc2:p:100:r:0)%
. suc(3) = 4 %(AxSucc3:p:100:r:0)%
. suc(4) = 5 %(AxSucc4:p:100:r:0)%
. suc(5) = 6 %(AxSucc5:p:100:r:0)%
. suc(6) = 7 %(AxSucc6:p:100:r:0)%
. suc(7) = 8 %(AxSucc7:p:100:r:0)%
. suc(8) = 9 %(AxSucc8:p:100:r:0)%
. suc(9) = x %(AxSucc9:p:100:r:0)%
. suc(x) = x1 %(AxSucc10:p:100:r:0)%
. suc(x1) = 0 %(AxSucc11:p:100:r:0)%
. not 0 = 1
. not 0 = 2
. not 0 = 3
. not 0 = 4
. not 0 = 5
. not 0 = 6
. not 0 = 7
. not 0 = 8
. not 0 = 9
. not 0 = x
. not 0 = x1
forall c, d: Note
. suc(c) = 0 <=> c = x1 %(AxSucc0-11:p:100:r:0)%
. suc(c) = suc(d) <=> c = d %(AxSuccEql:p:100:r:0)%
. c + 0 = c %(AxSuccDontKnow:p:100:r:0)%
. c + suc(d) = suc(c+d) %(AxSuccAdd:p:100:r:0)%
end
spec Chord = Symbols then
sort Chord
preds
hasAbsNote : Chord * Note
hasRelNote : Chord * Note
ops
root: Chord -> Note %(root_def)%
%% There must be a root note which is played, i.e., an absolute note.
forall c:Chord . exists n:Note
. root(c) = n /\ hasAbsNote(c,n) %(exOneRootThatMustBePlayed:p:-1)%
%% Relate absolute and relative notes
forall c:Chord,n:Note
. hasRelNote(c,n) <=> hasAbsNote(c,(root(c)+n)) %(reltoabs_note:p:-1)%
forall c: Chord . not (root(c) = 1 /\ hasAbsNote(c,7) /\ hasRelNote(c,7)) %(dis1:p:-1)%
forall c: Chord . not (root(c) = 1 /\ hasAbsNote(c,2)) %(dis2:p:-1)%
forall c: Chord . not (root(c) = 1 /\ hasAbsNote(c,4) /\ hasRelNote(c,4)) %(dis3:p:-1)%
forall c: Chord
. not (root(c) = 1 /\ hasAbsNote(c,7) /\ hasRelNote(c,6))
%% Define forbidden dissonances
forall n:Note, c:Chord
%% Two notes that can be interpreted as major and minor 3rd
. not (hasRelNote(c,3) /\ hasRelNote(c,4)) %(dis_minorMajorThird:p:-1)%
%% Two notes that can be interpreted as perfect and diminished 5th
. not (hasRelNote(c,7) /\ hasRelNote(c,6)) %(dis_perfectDimFifth:p:-1)%
%% One haftone away from the root is often quite dissonant
. not hasRelNote(c,1) %(dis_second:p:-1)%
%% A minor 7th (rel 10) with a major 6th (rel 9) is pretty dissonant
. not (hasRelNote(c,x) /\ hasRelNote(c,9)) %(dis_seventhsixth:p:-1)%
end
spec PerfCadence = Chord then
sort Perf
op p:Perf
op croot: Perf -> Note
op pre:Perf -> Chord
op rootpre:Perf -> Note
op post:Perf -> Chord
op rootpost:Perf -> Note
. hasRelNote(pre(p),0) %(Ax-relb0:p:2)%
. hasRelNote(pre(p),4) %(Ax-relb3:p:1)%
. hasRelNote(pre(p),7) %(Ax-relbb7:p:0)%
. hasRelNote(pre(p),x) %(Ax-relbb7:p:0)%
. hasRelNote(post(p),0) %(Ax-relb0:p:2)%
. hasRelNote(post(p),4) %(Ax-relb3:p:1)%
. hasRelNote(post(p),7) %(Ax-relbb7:p:0)%
. hasRelNote(post(p),x1) %(Ax-relbb7:p:0)%
. rootpre(p) = croot(p) + 7
. rootpost(p) = croot(p)
end
spec Progression =
PerfCadence then
List[sort Note] then
List[sort Chord] then
List[sort Perf] then
op c1,c2:Chord
op p: Perf
op lin:List[Note]
op lout:List[Chord]
op calc_prog: List[Note] -> List[Perf]
op calc_chord: List[Perf] -> List[Chord]
. calc_prog([]) = []
forall h:Note, t:List[Note]. calc_prog(h::t) = p::calc_prog(t)
. calc_chord([]) = []
forall h:Perf, t:List[Perf]. calc_chord(h::t) =
pre(p)::(post(p)::calc_chord(t))
. lout = calc_chord(calc_prog(lin))
end
spec CyclicGroup = Nat then
sort G < Nat
then List[sort G] then
op subseq: List[G]
op binop: G * G -> G
op ident: G
op inv: G -> G
pred gen: G
op size: Nat
op power: G * Nat -> G
op calc_subseq: G * G -> List[G]
forall x,y,z:G
. binop(x,binop(y,z)) = binop(binop(x,y),z) %assoc%
. forall x,y:G. exists n:Nat.
gen(y) => ((n<size) /\ power(y,n) = x)
end
spec Cyc12 = CyclicGroup then
op nongen: G
op seqall: G
. nongen = 4 as G
. seqall = 12 as G
. subseq = calc_subseq(nongen,seqall)
end
spec Gen =
sort H
then List[sort H] then
op l: List[H]
end
view I1: Gen to Progression =
H |-> Chord,
l |-> lout
view I2: Gen to Cyc12 =
H |-> G,
l |-> subseq
spec Blend = combine I1,I2