    --
    -- 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
    $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     -- 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
    $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 []

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