--
-- Copyright (c) 2005 Lennart Augustsson
-- See LICENSE for licensing details.
--
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 String
s) = String
s

data ConsDesc = ConsDesc String Int     -- name and arity
  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
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 []

-- Show formulae the LJT way
instance Show Formula where
  showsPrec :: Int -> Formula -> ShowS
showsPrec Int
_ (Conj [])  = String -> ShowS
showString String
"true"
  showsPrec Int
_ (Conj [Formula
c]) = Bool -> ShowS -> ShowS
showParen Bool
True (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"&" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Formula -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 Formula
c
  showsPrec Int
p (Conj [Formula]
cs)  = Bool -> ShowS -> ShowS
showParen (Int
pInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
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 [a
f]    = Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
41 a
f
          loop (a
f:[a]
fs) = Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
41 a
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" & " 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 String
"showsPrec Conj"
  showsPrec Int
_ (Disj [])      = String -> ShowS
showString String
"false"
  showsPrec Int
_ (Disj [(ConsDesc
_,Formula
c)]) = Bool -> ShowS -> ShowS
showParen Bool
True (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"|" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Formula -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 Formula
c
  showsPrec Int
p (Disj [(ConsDesc, Formula)]
ds)      = Bool -> ShowS -> ShowS
showParen (Int
pInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
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 [(a
_,a
f)]    = Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
31 a
f
          loop ((a
_,a
f):[(a, a)]
fs) = Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
31 a
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" 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 String
"showsPrec Disj"
  showsPrec Int
_ (Formula
f1 :-> Disj []) = String -> ShowS
showString String
"~" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Formula -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
100 Formula
f1
  showsPrec Int
p (Formula
f1 :-> Formula
f2) =
        Bool -> ShowS -> ShowS
showParen (Int
pInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
20) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> Formula -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
21 Formula
f1 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" -> " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Formula -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
20 Formula
f2
  showsPrec Int
p (PVar 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 Int
p (Var Symbol
s)      = Int -> Symbol -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Symbol
s
  showsPrec Int
p (Lam Symbol
s Term
e)    = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"\\" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Symbol -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 Symbol
s ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"." ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 Term
e
  showsPrec Int
p (Apply Term
f Term
a)  = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> Term -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
1 Term
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
2 Term
a
  showsPrec Int
_ (Cinj ConsDesc
_ Int
i)   = String -> ShowS
showString (String -> ShowS) -> String -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"Inj" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  showsPrec Int
_ (Ctuple Int
i)   = String -> ShowS
showString (String -> ShowS) -> String -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"Tuple" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  showsPrec Int
_ (Csplit Int
n)   = String -> ShowS
showString (String -> ShowS) -> String -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"split" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
  showsPrec Int
_ (Ccases [ConsDesc]
cds) = String -> ShowS
showString (String -> ShowS) -> String -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"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 Int
p (Xsel Int
i Int
n Term
e) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString (String
"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
"_" 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 String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> ShowS
forall a. Show a => Int -> a -> ShowS
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 (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
_            = []