-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathInput_XHtml.hs
84 lines (66 loc) · 2.65 KB
/
Input_XHtml.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
module Input_XHtml where
import Input
import FOL
import Control.Monad
import Data.Char
import Data.List
import Text.XHtml
instance HTML Input where
toHtml = runVars . inputToHtml 0
instance HTML Prop where
toHtml = runVars . propToHtml 0
inputToHtml :: Int -> Input -> Vars Html
inputToHtml n (Statement p) = propToHtml n p
inputToHtml n (YNQuest p) = liftM (\h -> "YNQ" +++ parens h) (propToHtml 0 p)
inputToHtml n (WhQuest q) = quant (toHtml "Which ") n q
inputToHtml n (CountQuest q) = quant (toHtml "Count ") n q
propToHtml :: Int -> Prop -> Vars Html
propToHtml _ (Pred x xs) = do xs' <- mapM expToHtml xs
return $ x +++ parens (concatHtml (intersperse (toHtml ",") xs'))
propToHtml n (And xs) = liftM (prec 1 n . intercalateWithSpace andHtml) $ mapM (propToHtml 1) xs
propToHtml n (Or xs) = liftM (prec 1 n . intercalateWithSpace orHtml) $ mapM (propToHtml 1) xs
propToHtml n (Imp x y) = binConn impHtml n x y
propToHtml n (Equiv x y) = binConn equivHtml n x y
propToHtml n (Equal x y) = infixPred (toHtml "=") n x y
propToHtml n (NotEqual x y) = infixPred (toHtml "!=") n x y
propToHtml n (Not x) = do x' <- propToHtml 2 x
return $ notHtml <+> x'
propToHtml n (All f) = quant forallHtml n f
propToHtml n (Exists f) = quant existsHtml n f
propToHtml n TrueProp = return $ emphasize << "true"
propToHtml n FalseProp = return $ emphasize << "false"
expToHtml :: Ind -> Vars Html
expToHtml (Const x) = return $ toHtml x
expToHtml (Var x) = return $ var x
var :: String -> Html
var x = emphasize << map toLower x
binConn :: Html -> Int -> Prop -> Prop -> Vars Html
binConn op n x y =
do x' <- propToHtml 1 x
y' <- propToHtml 1 y
return $ prec 1 n (x' <+> op <+> y')
infixPred :: Html -> Int -> Ind -> Ind -> Vars Html
infixPred p n x y =
do x' <- expToHtml x
y' <- expToHtml y
return $ prec 3 n (x' <+> p <+> y')
quant :: Html -> Int -> (Ind -> Prop) -> Vars Html
quant q n f =
do x <- getUnique
f' <- propToHtml 0 (f (Var x))
return $ prec 1 n (q +++ var x +++ "." <+> f')
prec :: Int -> Int -> Html -> Html
prec p n = if n >= p then parens else id
parens :: Html -> Html
parens x = "(" +++ x +++ ")"
(<+>) :: (HTML a, HTML b) => a -> b -> Html
x <+> y = x +++ " " +++ y
intercalateWithSpace :: (HTML a, HTML b) => a -> [b] -> Html
intercalateWithSpace x = concatHtml . intersperse (" " +++ x +++ " ") . map toHtml
impHtml = primHtmlChar "#8658"
equivHtml = primHtmlChar "#8660"
andHtml = primHtmlChar "#8743"
orHtml = primHtmlChar "#8744"
notHtml = primHtmlChar "#172"
forallHtml = primHtmlChar "#8704"
existsHtml = primHtmlChar "#8707"