在Haskell代码中找不到$ form的含义

Question

我正在遵循“ 实用逻辑和自动推理手册 ”的代码库的Haskell版本。以下情况的目的是什么$form？

eval :: Formula -> (Rel -> Bool) -> Bool
eval fm v = case fm of
  [$form| ? |] -> True
  [$form| ? |] -> False
  [$form| ^a |] -> v a
  [$form| ¬ $p |] -> not (eval p v)
  [$form| $p ? $q |] -> eval p v && eval q v
  [$form| $p ? $q |] -> eval p v || eval q v
  [$form| $p ? $q |] -> not (eval p v) || (eval q v)
  [$form| $p ? $q |] -> eval p v == eval q v
  _ -> error "quantifier in prop eval"

相关的OCaml代码很简单：

let rec eval fm v =
  match fm with
    False -> false
  | True -> true
  | Atom(x) -> v(x)
  | Not(p) -> not(eval p v)
  | And(p,q) -> (eval p v) & (eval q v)
  | Or(p,q) -> (eval p v) or (eval q v)
  | Imp(p,q) -> not(eval p v) or (eval q v)
  | Iff(p,q) -> (eval p v) = (eval q v);;

Answer 1

form是准报价单。这些提供了一种调用模板Haskell的方式，可以从您希望使用的任何其他类型的语法（例如本例中的Unicode逻辑公式）生成Haskell代码。

本质上，它只是用户可定义的语法糖：在实际编译之前，[$form| ? |]将被解析为pattern Top，[$form| $p ? $q |]pattern And p q等，即基本上与您在OCaml代码中具有的内容相同。可以说这对于此功能来说是过大的，但是当生成和/或匹配更复杂的公式时，这肯定会派上用场。

它是书面的[$form|，而不仅仅是[form|过时的GHC-6语法。对于当前的编译器，请使用后一种形式。