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