music_casl_pre.casl

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