module Djinn.LJTFormula(
Symbol(..),
Formula(..),
(<->),
(&),
(|:),
fnot,
false,
true,
ConsDesc(..),
Term(..), applys, freeVars
) where
import Data.List (union, (\\))
infixr 2 :->
infix 2 <->
infixl 3 |:
infixl 4 &
newtype Symbol = Symbol String
deriving (Symbol -> Symbol -> Bool
(Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool) -> Eq Symbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Symbol -> Symbol -> Bool
$c/= :: Symbol -> Symbol -> Bool
== :: Symbol -> Symbol -> Bool
$c== :: Symbol -> Symbol -> Bool
Eq, Eq Symbol
Eq Symbol =>
(Symbol -> Symbol -> Ordering)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Symbol)
-> (Symbol -> Symbol -> Symbol)
-> Ord Symbol
Symbol -> Symbol -> Bool
Symbol -> Symbol -> Ordering
Symbol -> Symbol -> Symbol
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Symbol -> Symbol -> Symbol
$cmin :: Symbol -> Symbol -> Symbol
max :: Symbol -> Symbol -> Symbol
$cmax :: Symbol -> Symbol -> Symbol
>= :: Symbol -> Symbol -> Bool
$c>= :: Symbol -> Symbol -> Bool
> :: Symbol -> Symbol -> Bool
$c> :: Symbol -> Symbol -> Bool
<= :: Symbol -> Symbol -> Bool
$c<= :: Symbol -> Symbol -> Bool
< :: Symbol -> Symbol -> Bool
$c< :: Symbol -> Symbol -> Bool
compare :: Symbol -> Symbol -> Ordering
$ccompare :: Symbol -> Symbol -> Ordering
$cp1Ord :: Eq Symbol
Ord)
instance Show Symbol where
show :: Symbol -> String
show (Symbol s :: String
s) = String
s
data ConsDesc = ConsDesc String Int
deriving (ConsDesc -> ConsDesc -> Bool
(ConsDesc -> ConsDesc -> Bool)
-> (ConsDesc -> ConsDesc -> Bool) -> Eq ConsDesc
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConsDesc -> ConsDesc -> Bool
$c/= :: ConsDesc -> ConsDesc -> Bool
== :: ConsDesc -> ConsDesc -> Bool
$c== :: ConsDesc -> ConsDesc -> Bool
Eq, Eq ConsDesc
Eq ConsDesc =>
(ConsDesc -> ConsDesc -> Ordering)
-> (ConsDesc -> ConsDesc -> Bool)
-> (ConsDesc -> ConsDesc -> Bool)
-> (ConsDesc -> ConsDesc -> Bool)
-> (ConsDesc -> ConsDesc -> Bool)
-> (ConsDesc -> ConsDesc -> ConsDesc)
-> (ConsDesc -> ConsDesc -> ConsDesc)
-> Ord ConsDesc
ConsDesc -> ConsDesc -> Bool
ConsDesc -> ConsDesc -> Ordering
ConsDesc -> ConsDesc -> ConsDesc
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ConsDesc -> ConsDesc -> ConsDesc
$cmin :: ConsDesc -> ConsDesc -> ConsDesc
max :: ConsDesc -> ConsDesc -> ConsDesc
$cmax :: ConsDesc -> ConsDesc -> ConsDesc
>= :: ConsDesc -> ConsDesc -> Bool
$c>= :: ConsDesc -> ConsDesc -> Bool
> :: ConsDesc -> ConsDesc -> Bool
$c> :: ConsDesc -> ConsDesc -> Bool
<= :: ConsDesc -> ConsDesc -> Bool
$c<= :: ConsDesc -> ConsDesc -> Bool
< :: ConsDesc -> ConsDesc -> Bool
$c< :: ConsDesc -> ConsDesc -> Bool
compare :: ConsDesc -> ConsDesc -> Ordering
$ccompare :: ConsDesc -> ConsDesc -> Ordering
$cp1Ord :: Eq ConsDesc
Ord, Int -> ConsDesc -> ShowS
[ConsDesc] -> ShowS
ConsDesc -> String
(Int -> ConsDesc -> ShowS)
-> (ConsDesc -> String) -> ([ConsDesc] -> ShowS) -> Show ConsDesc
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConsDesc] -> ShowS
$cshowList :: [ConsDesc] -> ShowS
show :: ConsDesc -> String
$cshow :: ConsDesc -> String
showsPrec :: Int -> ConsDesc -> ShowS
$cshowsPrec :: Int -> ConsDesc -> ShowS
Show)
data Formula = Conj [Formula]
| Disj [(ConsDesc, Formula)]
| Formula :-> Formula
| PVar Symbol
deriving (Formula -> Formula -> Bool
(Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool) -> Eq Formula
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Formula -> Formula -> Bool
$c/= :: Formula -> Formula -> Bool
== :: Formula -> Formula -> Bool
$c== :: Formula -> Formula -> Bool
Eq, Eq Formula
Eq Formula =>
(Formula -> Formula -> Ordering)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Formula)
-> (Formula -> Formula -> Formula)
-> Ord Formula
Formula -> Formula -> Bool
Formula -> Formula -> Ordering
Formula -> Formula -> Formula
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Formula -> Formula -> Formula
$cmin :: Formula -> Formula -> Formula
max :: Formula -> Formula -> Formula
$cmax :: Formula -> Formula -> Formula
>= :: Formula -> Formula -> Bool
$c>= :: Formula -> Formula -> Bool
> :: Formula -> Formula -> Bool
$c> :: Formula -> Formula -> Bool
<= :: Formula -> Formula -> Bool
$c<= :: Formula -> Formula -> Bool
< :: Formula -> Formula -> Bool
$c< :: Formula -> Formula -> Bool
compare :: Formula -> Formula -> Ordering
$ccompare :: Formula -> Formula -> Ordering
$cp1Ord :: Eq Formula
Ord)
(<->) :: Formula -> Formula -> Formula
x :: Formula
x <-> :: Formula -> Formula -> Formula
<-> y :: Formula
y = (Formula
xFormula -> Formula -> Formula
:->Formula
y) Formula -> Formula -> Formula
& (Formula
yFormula -> Formula -> Formula
:->Formula
x)
(&) :: Formula -> Formula -> Formula
x :: Formula
x & :: Formula -> Formula -> Formula
& y :: Formula
y = [Formula] -> Formula
Conj [Formula
x, Formula
y]
(|:) :: Formula -> Formula -> Formula
x :: Formula
x |: :: Formula -> Formula -> Formula
|: y :: Formula
y = [(ConsDesc, Formula)] -> Formula
Disj [((String -> Int -> ConsDesc
ConsDesc "Left" 1), Formula
x), ((String -> Int -> ConsDesc
ConsDesc "Right" 1), Formula
y)]
fnot :: Formula -> Formula
fnot :: Formula -> Formula
fnot x :: Formula
x = Formula
x Formula -> Formula -> Formula
:-> Formula
false
false :: Formula
false :: Formula
false = [(ConsDesc, Formula)] -> Formula
Disj []
true :: Formula
true :: Formula
true = [Formula] -> Formula
Conj []
instance Show Formula where
showsPrec :: Int -> Formula -> ShowS
showsPrec _ (Conj []) = String -> ShowS
showString "true"
showsPrec _ (Conj [c :: Formula
c]) = Bool -> ShowS -> ShowS
showParen Bool
True (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString "&" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Formula -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 0 Formula
c
showsPrec p :: Int
p (Conj cs :: [Formula]
cs) = Bool -> ShowS -> ShowS
showParen (Int
pInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>40) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [Formula] -> ShowS
forall a. Show a => [a] -> ShowS
loop [Formula]
cs
where loop :: [a] -> ShowS
loop [f :: a
f] = Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 41 a
f
loop (f :: a
f:fs :: [a]
fs) = Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 41 a
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " & " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
loop [a]
fs
loop [] = String -> ShowS
forall a. HasCallStack => String -> a
error "showsPrec Conj"
showsPrec _ (Disj []) = String -> ShowS
showString "false"
showsPrec _ (Disj [(_,c :: Formula
c)]) = Bool -> ShowS -> ShowS
showParen Bool
True (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString "|" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Formula -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 0 Formula
c
showsPrec p :: Int
p (Disj ds :: [(ConsDesc, Formula)]
ds) = Bool -> ShowS -> ShowS
showParen (Int
pInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>30) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [(ConsDesc, Formula)] -> ShowS
forall a a. Show a => [(a, a)] -> ShowS
loop [(ConsDesc, Formula)]
ds
where loop :: [(a, a)] -> ShowS
loop [(_,f :: a
f)] = Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 31 a
f
loop ((_,f :: a
f):fs :: [(a, a)]
fs) = Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 31 a
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " v " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, a)] -> ShowS
loop [(a, a)]
fs
loop [] = String -> ShowS
forall a. HasCallStack => String -> a
error "showsPrec Disj"
showsPrec _ (f1 :: Formula
f1 :-> Disj []) = String -> ShowS
showString "~" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Formula -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 100 Formula
f1
showsPrec p :: Int
p (f1 :: Formula
f1 :-> f2 :: Formula
f2) =
Bool -> ShowS -> ShowS
showParen (Int
pInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>20) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> Formula -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 21 Formula
f1 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " -> " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Formula -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 20 Formula
f2
showsPrec p :: Int
p (PVar s :: Symbol
s) = Int -> Symbol -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Symbol
s
data Term = Var Symbol
| Lam Symbol Term
| Apply Term Term
| Ctuple Int
| Csplit Int
| Cinj ConsDesc Int
| Ccases [ConsDesc]
| Xsel Int Int Term
deriving (Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq, Eq Term
Eq Term =>
(Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
$cp1Ord :: Eq Term
Ord)
instance Show Term where
showsPrec :: Int -> Term -> ShowS
showsPrec p :: Int
p (Var s :: Symbol
s) = Int -> Symbol -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Symbol
s
showsPrec p :: Int
p (Lam s :: Symbol
s e :: Term
e) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString "\\" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Symbol -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 0 Symbol
s ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString "." ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 0 Term
e
showsPrec p :: Int
p (Apply f :: Term
f a :: Term
a) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> Term -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 1 Term
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 2 Term
a
showsPrec _ (Cinj _ i :: Int
i) = String -> ShowS
showString (String -> ShowS) -> String -> ShowS
forall a b. (a -> b) -> a -> b
$ "Inj" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
showsPrec _ (Ctuple i :: Int
i) = String -> ShowS
showString (String -> ShowS) -> String -> ShowS
forall a b. (a -> b) -> a -> b
$ "Tuple" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
showsPrec _ (Csplit n :: Int
n) = String -> ShowS
showString (String -> ShowS) -> String -> ShowS
forall a b. (a -> b) -> a -> b
$ "split" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
showsPrec _ (Ccases cds :: [ConsDesc]
cds) = String -> ShowS
showString (String -> ShowS) -> String -> ShowS
forall a b. (a -> b) -> a -> b
$ "cases" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([ConsDesc] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ConsDesc]
cds)
showsPrec p :: Int
p (Xsel i :: Int
i n :: Int
n e :: Term
e) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString ("sel_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 2 Term
e
applys :: Term -> [Term] -> Term
applys :: Term -> [Term] -> Term
applys f :: Term
f as :: [Term]
as = (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term -> Term -> Term
Apply Term
f [Term]
as
freeVars :: Term -> [Symbol]
freeVars :: Term -> [Symbol]
freeVars (Var s :: Symbol
s) = [Symbol
s]
freeVars (Lam s :: Symbol
s e :: Term
e) = Term -> [Symbol]
freeVars Term
e [Symbol] -> [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol
s]
freeVars (Apply f :: Term
f a :: Term
a) = Term -> [Symbol]
freeVars Term
f [Symbol] -> [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a] -> [a]
`union` Term -> [Symbol]
freeVars Term
a
freeVars (Xsel _ _ e :: Term
e) = Term -> [Symbol]
freeVars Term
e
freeVars _ = []