Логическое сопоставление с образцом в Why3ML

Question

В других ML-вариантах (таких как SML) можно сделать что-то вроде этого:

case l of
   (true, _) => false
 | (false,true) => false
 | (false,false) => true

Тем не менее, делая аналогичные вещи, используя Why3ML match объявление вызывает синтаксическую ошибку:

match l with
 | (true, _) -> false
 | (false,true) -> false
 | (false,false) -> true
end

Как правильно выполнить сопоставление с шаблоном на основе значений внутри кортежа?

Answer 1

Да, это возможно

module Test
  let unpack_demo () =
    let tup = (true, false) in (* parens required here! *)
    match tup with
    | True, False -> true  (* pattern must use bool's constructor tags *)
    | _           -> false
    end

  let ex2 () = match true, false with (* parens not required here *)
    | True, x      -> x
    | False, True  -> false
    | False, False -> true
    end
end

hayai[cygwin64][1155]:~/prog/why3$ why3 execute test.mlw Test.unpack_demo
Execution of Test.unpack_demo ():
     type: bool
   result: true
  globals:

hayai[cygwin64][1156]:~/prog/why3$ why3 execute test.mlw Test.ex2
Execution of Test.ex2 ():
     type: bool
   result: false
  globals:

Язык шаблонов Why3 довольно прост по сравнению с SML или OCaml. Единственными значениями, разрешенными в шаблонах Why3, являются конструкторы (даже не допускаются, например, целочисленные константы), и только кортежи могут быть деструктурированы. Вот почему True а также False используются в шаблонах выше; на самом деле они являются правильными конструкторами для bool-true а также false существуют для удобства, но они не будут работать в шаблонах. Смотрите рисунок 7.2 в справочнике по грамматике и посмотрите на определение pattern,