在水星中匹配一個lambda和一個謂詞的確定性

在Mercury中，我可以聲明一個lambda具有與包含lambda的謂詞模式相同的決定性嗎？在水星中匹配一個lambda和一個謂詞的確定性

這是我正在嘗試做的。我寫了一個摺疊函數（下面），它適用於array2d類型。 fold爲數組中的每個元素調用一個調用者提供的謂詞。它工作正常，只要它只接受一個det謂詞作爲參數。

:- pred fold(array2d(T), pred(T, int, int, A, A),    A, A). 
:- mode fold(in,   pred(in, in, in, in, out) is det,  in, out) is det. 
% Uncommenting the next line causes mode errors during compilation 
% :- mode fold(in,  pred(in, in, in, in, out) is semidet, in, out) is semidet. 

fold(Array, Pred, !Accumulator) :- 
    bounds(Array, NumRows, NumCols), 

    FoldRows = (pred(RowNumber :: in, RowAccIn :: in, RowAccOut :: out) is det :- 
     FoldCols = (pred(ColNumber :: in, ColAccIn :: in, ColAccOut :: out) is det :- 
      Value = Array^elem(RowNumber, ColNumber), 
      Pred(Value, RowNumber, ColNumber, ColAccIn, ColAccOut) 
     ), 
     int.fold_up(FoldCols, 0, NumCols - 1, RowAccIn, RowAccOut) 
    ), 
    int.fold_up(FoldRows, 0, NumRows - 1, !Accumulator).

但我想fold來接受一個DET或semidet謂詞（如果謂詞任何調用失敗，失敗）。取消註釋mode ... is semidet行給我編譯器錯誤，我不知道如何解決。問題是fold中的lambda表達式被聲明爲det，所以他們不能調用semidet Pred。如果我將lambda轉換爲semidet，那麼整個fold不能被det。

我該如何解決這個問題？看起來最直接的方法是聲明lambda表達式繼承它們的謂詞決定論 - 所以它們在fold被用作det時也是如此，但是我不知道這是否可能。

當然，另一種方法是將FoldRows和FoldCols轉換爲具有多種模式的命名謂詞（不是lambda表達式）。但這很快就變得不雅，我想知道是否有更直接的解決方案。

來源

2014-10-31 Evan

水星有時可以推斷謂詞的模式和決定論，所以我最初嘗試通過從lambda表達式中省略決定論聲明。然而Mercury的lambda語法不允許我這樣做，所以這個推理不能用於lambda表達式。

恐怕唯一的解決方法就是，如您所猜，將FoldRows和FoldCols轉換爲多模式命名謂詞。

來源

2014-11-04 03:04:36

在水星中匹配一個lambda和一個謂詞的確定性

回答

相關問題