    --
    -- 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 s :: 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
    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 []

    -- Show formulae the LJT way
    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 _            = []