Geo*_*nat 1 forms logic haskell logical-operators
我有以下内容:
type Name = String
data Prop
= Var Name
| F
| T
| Not Prop
| Prop :|: Prop
| Prop :&: Prop
deriving (Eq, Read)
infixr 2 :|:
Run Code Online (Sandbox Code Playgroud)
Prop类型代表命题公式.命题变量,例如p和q可以用Var"p"和Var"q"表示.
F和T是False和True的常数布尔值.
不代表否定(〜或¬)
:|:和:&:表示析取(/)和结合(/ \)
我们可以写出逻辑命题:
( Var "p" :|: Var "q") :&: ( Not (Var "p") :&: Var "q")
Run Code Online (Sandbox Code Playgroud)
我要做的是:通过使Prop成为Show类的实例,替换Not,:|:和:&:with~,/和/ \,以便以下内容为真:
test_ShowProp :: Bool
test_ShowProp =
show (Not (Var "P") :&: Var "Q") == "((~P)/\Q)"
Run Code Online (Sandbox Code Playgroud)
这是我到目前为止的实现:
instance Show Prop where
show (Var p) = p
show (Not (Var p)) = "(~" ++ p ++ ")"
show (Var p :|: Var q) = p ++ "\\/" ++ q
show (Var p :&: Var q) = p ++ "/\\" ++ q
Run Code Online (Sandbox Code Playgroud)
但这并不包括所有情况,只包括基本情况.我应该如何继续实施,以便解决任何命题公式,而不仅仅是硬编码公式?因为此刻
(Var "p" :&: Var "q")
Run Code Online (Sandbox Code Playgroud)
输出:p /\q
但
Not (Var "p" :&: Var "q")
Run Code Online (Sandbox Code Playgroud)
输出:功能中的非详尽模式显示
您应该只匹配公式的一个"层",即只匹配一个构造函数,并利用子公式的递归.例如,
show (Not f) = "(~" ++ show f ++ ")"
Run Code Online (Sandbox Code Playgroud)
将适用于以否定开头的任何公式,即使在该否定下存在非变量子公式.
正确地获得括号可能会很棘手.你需要慷慨的括号或定义showsPrec.如果你是初学者,我会推荐前者,它不需要处理优先级.