кастинг в реализации gflist_vt_mergesort$cmp

В gflist_vt.sats подпись gflist_vt_mergesort$cmp подразумевает, что порядок, используемый для сортировки, должен быть таким же, как и для штампа. Я так понимаю, что если такая функция сравнения задана, то надежность функции обеспечена.

В этом примере gflist_vt_mergesort$cmp кажется для реализации с использованием небезопасного приведения.

  • Безопасно ли это делать? (т. е. не вызывает ли это каких-либо проблем? например, что, если список отсортирован несколько раз с разным порядком?)
  • Есть ли другой (более безопасный) способ?

ats
person CoiL    schedule 29.01.2017    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Небезопасное приведение по своей сути небезопасно.

Небезопасное литье можно удалить. Для этого вам необходимо реализовать абстрактный тип stamped_vt0ype (которому присвоен псевдоним stamped_vt). Например, чтобы отсортировать список целых чисел в порядке убывания, вы можете сделать следующее:

local

assume stamped_vt0ype(_, i) = int(~i)

in (* in-of-local *)

implement
{a}
gflist_vt_mergesort$cmp(x, y) = g1int_sgn(y - x)

end // end of [local]

Однако выполнение чего-то подобного, похоже, мало что дает с точки зрения практического программирования.

person Hongwei Xi    schedule 30.01.2017