Definition keyAssignmentEvaluateFull
  (key        : nat)
  (velocity   : R)
  (assignment : keyAssignment)
: option keyEvaluation :=
  match keyAssignmentMatchesDecidable key velocity assignment with
  | right _ => None
  | left p  =>
    let clip  := kaClipId assignment in
    let ampV  := keyAssignmentEvaluateAmplitudeForVelocity velocity assignment in
    let ampVP := keyAssignmentEvaluateAmplitudeForVelocityNormalized _ _ _ p in
    let ampK  := keyAssignmentEvaluateAmplitudeForKey key assignment in
    let ampKP := keyAssignmentEvaluateAmplitudeForKeyNormalized _ _ _ p in
    let rate  := keyAssignmentEvaluateRate key assignment in
    let rateP := keyAssignmentEvaluateRateNonNegative _ _ _ p in
      Some (keyEvaluationMake clip ampV ampVP ampK ampKP rate rateP)
  end.
