module Lab3 where
import Data.List

{-
一个布尔表达式就像一个算术表达式，只是这里的值都是布尔值True和False，
其中的变量也只能代入布尔值，各种运算用运算表给出。
布尔表达式的另一种解读是表示命题，如文件lab3.pdf所讲。
如果不理解命题，就看作布尔表达式好了。
本作业要求判断一个布尔表达式是不是永真式：即无论将变量代入什么值，其结果总是True。
一、定义命题类型及其Show特例
命题的集合可以如下定义
-真命题(记作T)和假命题(记作F)是命题；
-由一个字母表示的命题变元是一个命题；
-如果P是命题,则它的否定是一个命题,记作~P；"~"称为否定联结词；
-如果p,q是命题,则它们的合取是一个命题,记作p&&q; "&&"称为合取联结词；
-如果p,q是命题,则它们的析取是一个命题,记作p||q; "||"称为析取联结词；
-如果p,q是命题,则它们的蕴含是一个命题,记作p=>q; "=>"称为蕴含联结词；
-所有的命题由以上规则经过有限步生成。
所以,命题的集合是一个归纳定义的集合,可以用代数类型描述：
-}
data Prop=Const Bool
    | Var Char
    | Not Prop
    | And Prop Prop
    | Or Prop Prop
    | Imply Prop Prop
    deriving Eq

{-
习题1
试将类型Prop定义成类Show的特例,使得Prop中元素能够显示成定义中我们习惯的表示。
例如,Var 'A',And (Var 'P') (Var 'Q')分别显示成A和P&&Q等。
-}
instance Show Prop where
    show (Const True)="True"
    show (Const False)="False"
    show (Var x)=[x]
    show (Not x)="~"++show x
    show (And x y)=(show x)++"&&"++(show y)
    show (Or x y)=(show x)++"||"++(show y)
    show (Imply x y)=(show x)++"=>"++(show y)

{-
习题2
定义下列值p1,p2,p3::Prop
使得它们个表示下列命题:
A&&~A
A||~A
A=>(A&&B)
-}
p1=And (Var 'A') (Not (Var 'A'))
p2=Or (Var 'A') (Not (Var 'A'))
p3=Imply (Var 'A') (And (Var 'A') (Var 'B'))

{-
二、命题真值表
一个命题或者真,或者假。
例如,不包含变元的命题T表示真命题,命 题F表示假命题。
包含变元的命题的真假依赖于变元表示命题的真假,
所以,一个命题可以看作它包含的变元的函数,称为真值函数,
其中每个变元的取 值为真或者假,分别用TVue和False表示。
每个命题的取值和其中变元的关系可以用一个表来表示,称之为命题函数的真值表。
以下是命题联结词的真值表：
对应任意的命题函数，给定变元的一个代换，根据上述真值表可计算相应的真值。
例如,命题p3:A=>(A && B)在代换[('A',True),('B',False)]的真值是False。
我们可以用下列类型表示代换：
-}
type Subst=[(Char,Bool)]

{-
习题3
试根据以上解释定义函数:
-}
eval::Subst->Prop->Bool

{-
例如
>eval [('A',True),('B',False)] p3
False
-}
eval sub (Const p)=p
eval sub (Var p)=(getBool sub p) where
    getBool sub x=
        if length xs >1
            then error "Variable has more than 2 values."
            else head xs
        where xs=[k|(y,k)<-sub,x==y]
eval sub (Not p)=not (eval sub p)
eval sub (And p q)=(eval sub p)&&(eval sub q)
eval sub (Or p q)=(eval sub p)||(eval sub q)
eval sub (Imply p q)=((eval sub p)&&(eval sub q))||(not (eval sub p))

{-
习题4
试定义下列函数：
-}
vars::Prop->[Char]
substs::Prop->[Subst]

{-
其中vars p给出命题p中出现的所有不同变元,substs p给出命题p中变元的所有可能代换。例如
vars p3=['A','B']
substs p3=
    [
        [('A',True),('B',True)],
        [('A',True),('B',False)],
        [('A',False),('B',True)],
        [('A',False),('B',False)]
    ]
-}
vars (Const x)=[]
vars (Var x)=[x]
vars (Not p)=vars p
vars (And p q)=nub((vars p)++(vars q))
vars (Or p q)=nub((vars p)++(vars q))
vars (Imply p q)=nub((vars p)++(vars q))

substs p=getsub (vars p) where
    getsub []=[]
    getsub [x]=[[(x,True)]]++[[(x,False)]]
    getsub (x:xs)=[(x,True):a|a<-getsub(xs)]++[(x,False):a|a<-getsub(xs)]

{-
三、定义一个判断命题是否永真的函数
如果一个命题函数在变元的任意代换下真值是True,则称之为永真式。
例如,命题p2是永真式。
试定义判定一个命题是否永真式的函数,并说明你的函 数定义的正确性：
习题5
-}
isTaut::Prop->Bool

{-
例如
>isTaut p1
False
>isTaut p2
True
-}
isTaut p=testisTaut p (substs p) where
    testisTaut p [x]=(eval x p)
    testisTaut p (x:xs)=if (eval x p) then testisTaut p xs else False