forked from GitHub/gf-core
79 lines
1.6 KiB
Haskell
79 lines
1.6 KiB
Haskell
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)))))
|
|
|