mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 13:09:33 -06:00
102 lines
2.2 KiB
Haskell
102 lines
2.2 KiB
Haskell
module Logic where
|
|
|
|
data Prop =
|
|
Pred Ident [Exp]
|
|
| And Prop Prop
|
|
| Or Prop Prop
|
|
| If Prop Prop
|
|
| Not Prop
|
|
| All Prop
|
|
| Exist Prop
|
|
deriving Show
|
|
|
|
data Exp =
|
|
App Ident [Exp]
|
|
| Var Int -- de Bruijn index
|
|
deriving Show
|
|
|
|
type Ident = String
|
|
|
|
data Model a = Model {
|
|
app :: Ident -> [a] -> a,
|
|
prd :: 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
|
|
App f xs -> app model f (map (valExp model assign) xs)
|
|
Var i -> look i assign
|
|
|
|
valProp :: Model a -> Assignment a -> Prop -> Bool
|
|
valProp model assign prop = case prop of
|
|
Pred f xs -> prd 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
|
|
|
|
liftProp :: Int -> Prop -> Prop
|
|
liftProp i p = case p of
|
|
Pred f xs -> Pred f (map liftExp xs)
|
|
And a b -> And (lift a) (lift b)
|
|
Or a b -> Or (lift a) (lift b)
|
|
If a b -> If (lift a) (lift b)
|
|
Not a -> Not (lift a)
|
|
All p -> All (liftProp (i+1) p)
|
|
Exist p -> Exist (liftProp (i+1) p)
|
|
where
|
|
lift = liftProp i
|
|
liftExp e = case e of
|
|
App f xs -> App f (map liftExp xs)
|
|
Var j -> Var (j + i)
|
|
_ -> e
|
|
|
|
|
|
-- example: initial segments of integers
|
|
|
|
intModel :: Int -> Model Int
|
|
intModel mx = Model {
|
|
app = \f xs -> case (f,xs) of
|
|
("+",_) -> sum xs
|
|
(_,[]) -> read f,
|
|
prd = \f xs -> case (f,xs) of
|
|
("E",[x]) -> even x
|
|
("<",[x,y]) -> x < y
|
|
("=",[x,y]) -> x == y
|
|
_ -> error "undefined val",
|
|
dom = [0 .. mx]
|
|
}
|
|
|
|
exModel = intModel 100
|
|
|
|
ev x = Pred "E" [x]
|
|
lt x y = Pred "<" [x,y]
|
|
eq x y = Pred "=" [x,y]
|
|
int i = App (show i) []
|
|
|
|
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) (int 100)) (Exist (lt (Var 1) (Var 0))))
|
|
|
|
ex4 :: Prop
|
|
ex4 = All (All (If (lt (Var 1) (Var 0)) (Not (lt (Var 0) (Var 1)))))
|
|
|