Я попытался реализовать алгоритм MAA с помощью Cryptol. Вот что я сделал до сих пор, но мне не повезло. Любые идеи?
main: ([32], [32]) -> [32]
main (x , y) = add (x , y)x
where x = (take`{16} xy, drop`{16} xy)
where xy = mul1 (x , y)
mul1: ([32] ,[32]) -> [32]
mul1 (x , y) = xy
where xy = x * y
add: ([16] ,[16]) -> [16]
add (x , y) = xy
where xy = x + y
add
принимает один аргумент кортежа, а не два аргумента. Вы также скрываете имена переменных, используйте уникальные имена в main
.
В вашем главном есть несколько ошибок.
add (x , y)x
Сказать что? Слишком много доводовmain (x , y) = ...
и where x = ...
Ну что теперь x равно? Не затеняйте имена переменных, если можете.where x = ...
и where xy = ...
Используйте одиночный `where вместо вложенного просто для чистоты, а?Наконец, есть ошибка типа. Добавление дает вам 16-битное число (посмотрите на сигнатуру типа), поэтому его результат также не может быть результатом main
, тип которого указывает, что он возвращает 32-битное число. 32 не равно 16. Я исправил это и вышеизложенное, просто изменив тип main
, но это, вероятно, не то, что вы хотите, поэтому вам нужно добавить здесь любую логику, которую вы хотите (например, нулевое расширение или знак продлить?).
Код:
main: ([32], [32]) -> [16]
main (x , y) = add xy16
where xy16 = (take`{16} xy, drop`{16} xy)
xy = mul1 (x , y)
mul1: ([32] ,[32]) -> [32]
mul1 (x , y) = xy
where xy = x * y
add: ([16] ,[16]) -> [16]
add (x , y) = xy
where xy = x + y
Предположительно, это урезанная версия вашей исходной проблемы, но если вы не заметили, вам действительно не нужно определять функцию add
только для использования +
, и то же самое касается mul
. Также вам не нужны явные аннотации типов для take
и drop
, поскольку они могут быть выведены. Например:
main2 : [32] -> [32] -> [16]
main2 x y = take xy + drop xy where xy = x * y
И тогда мы можем сделать очевидное:
Main> :prove \x y -> main (x,y) == main2 x y
Q.E.D.
Большое спасибо. Я ценю это!
Какая у вас ошибка?