blob: e3d72f06906b597bed52fe23df9f6e70076c8836 (
plain)
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
|
module Logic where
data Prop =
Atom Ident [Exp]
| And Prop Prop
| Or Prop Prop
| If Prop Prop
| Not Prop
| All Prop
| Exist Prop
deriving Show
data Exp =
Const Ident
| Var Int -- de Bruijn index
deriving Show
type Ident = String
data Model a = Model {
ind :: Ident -> a,
val :: Ident -> [a] -> Bool,
dom :: [a]
}
type Assignment a = [a]
update :: a -> Assignment a -> Assignment a
update x assign = x : assign
look :: Int -> Assignment a -> a
look i assign = assign !! i
valExp :: Model a -> Assignment a -> Exp -> a
valExp model assign exp = case exp of
Const c -> ind model c
Var i -> look i assign
valProp :: Model a -> Assignment a -> Prop -> Bool
valProp model assign prop = case prop of
Atom f xs -> val model f (map (valExp model assign) xs)
And a b -> v a && v b
Or a b -> v a || v b
If a b -> if v a then v b else True
Not a -> not (v a)
All p -> all (\x -> valProp model (update x assign) p) (dom model)
Exist p -> any (\x -> valProp model (update x assign) p) (dom model)
where
v = valProp model assign
intModel :: Int -> Model Int
intModel mx = Model {
ind = read,
val = \f xs -> case (f,xs) of
("E",[x]) -> even x
("<",[x,y]) -> x < y
_ -> error "undefined val",
dom = [0 .. mx]
}
exModel = intModel 100
ev x = Atom "E" [x]
lt x y = Atom "<" [x,y]
ex1 :: Prop
ex1 = Exist (ev (Var 0))
ex2 :: Prop
ex2 = All (Exist (lt (Var 1) (Var 0)))
ex3 :: Prop
ex3 = All (If (lt (Var 0) (Const "100")) (Exist (lt (Var 1) (Var 0))))
ex4 :: Prop
ex4 = All (All (If (lt (Var 1) (Var 0)) (Not (lt (Var 0) (Var 1)))))
|
