Skip to content

Commit

Permalink
Rename MIDI to MusicalInstrumentDigitalInterface
Browse files Browse the repository at this point in the history
  • Loading branch information
ngeiswei committed Jun 13, 2024
1 parent 03be365 commit 121f5ad
Showing 1 changed file with 16 additions and 23 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -85,35 +85,26 @@
;; 3.4. Cov for contravariant.

;; Subtyping is relexive
(: STRefl (<: $T $T))
!(add-atom &kb (: STRefl (<: $T $T)))

;; Subtyping is transitive
(: STTrans (->
;; Premises
(<: $S $T)
(<: $T $U)
;; Conclusion
(<: $S $U)))
!(add-atom &kb (: STTrans (-> (<: $S $T)
(-> (<: $T $U)
(<: $S $U)))))

;; Subtyping of function types is contravariant over inputs and
;; covariant over outputs.
(: STConv (->
;; Premises
(<: $T1 $S1)
(<: $S2 $T2)
;; Conclusion
(<: (-> $S1 $S2) (-> $T1 $T2))))
!(add-atom &kb (: STConv (-> (<: $T1 $S1)
(-> (<: $S2 $T2)
(<: (-> $S1 $S2) (-> $T1 $T2))))))

;; Relationship between subtyping and type assume explicit coercion.
;; That is if a term `t` is of type `S` a subtype of `T`, then
;; `(coerce proof_S<:T t)` is of type `T`, where `proof_S<:T` is a
;; proof that `S` is a subtype of `T`.
(: coerce (->
;; Premises
(<: $S $T)
$S
;; Conclusion
$T))
!(add-atom &kb (: coerce (-> (<: $S $T)
(-> $S
$T))))

;;;;;;;;;;;;;;
;; Ontology ;;
Expand All @@ -134,7 +125,7 @@
!(add-atom &kb (: US (<: UniformResourceLocator String))) ; SUMO

;; MIDI
!(add-atom &kb (: MB (<: MIDI Bytes)))
!(add-atom &kb (: MB (<: MusicalInstrumentDigitalInterface Bytes)))

;; Audio
!(add-atom &kb (: AB (<: Audio Bytes)))
Expand Down Expand Up @@ -198,7 +189,7 @@
;; Define midi2voice-zh.singingZH service method
!(add-atom &kb (: midi2voice-zh.singingZH
(-> Text
(-> MIDI
(-> MusicalInstrumentDigitalInterface
Audio))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
Expand Down Expand Up @@ -271,7 +262,7 @@
;;;;;;;;;;;;

;; Method
!(add-atom &kb (: tomidi.a2m (-> Audio MIDI)))
!(add-atom &kb (: tomidi.a2m (-> Audio MusicalInstrumentDigitalInterface)))

;;;;;;;;;;;
;; Mixer ;;
Expand Down Expand Up @@ -652,7 +643,9 @@
(: (sound-spleeter.Output.accomp
(: (S' Z') sound-spleeter.Output)) Audio))
(: ((midi2voice-zh.singingZH (: (S' (S' (S' Z'))) Text))
(: (tomidi.a2m (: (S' (S' Z')) Audio)) MIDI)) Audio)))
(: (tomidi.a2m (: (S' (S' Z')) Audio))
MusicalInstrumentDigitalInterface))
Audio)))
(: (((machine-translation.translate
(: "English" NaturalLanguage))
(: "Chinese" NaturalLanguage))
Expand Down

0 comments on commit 121f5ad

Please sign in to comment.