{-# OPTIONS_GHC -fdefer-typed-holes #-}

import Ersatz
import Prelude hiding (and, not, (||), (&&), not, product)
import Ersatz.Relation as R hiding (transitive)
import Ersatz.Solver
import Ersatz.Solver.Minisat
import qualified Data.Array as A

-- naive implementation (n^4 formula size)
transitive_closure_naive :: A.Ix a => Relation a a -> Relation a a
transitive_closure_naive r =
  let ((l,_),(h,_)) = bounds r
      e = A.rangeSize (l,h) -- discuss: is this the correct choice?
  in  iterate (\ s -> R.union r (R.product r s)) r !! e


transitive_closure_cubic :: A.Ix a => Relation a a -> Relation a a
transitive_closure_cubic r =
  let ((l,_),(h,_)) = bounds r
      bnd = ((l,l,l),(h,h,h))
      get p x q = if x < l then r ! (p,q) else a A.! (p,x,q)
      a = A.array bnd $ do
        i@(p,x,q) <- A.range bnd
        return (i, get _ _ _ || _ && _)
  in  buildFrom (\ p q -> get p h q) (bounds r)


transitive_closure :: A.Ix a => Relation a a -> Relation a a
transitive_closure = transitive_closure_naive


transitive_reflexive_closure :: A.Ix a => Relation a a -> Relation a a
transitive_reflexive_closure r =
  R.union (R.identity $ bounds r) $ transitive_closure r

diamond :: A.Ix a => Relation a a -> Bit
diamond r =
  R.product (R.mirror r) r `R.implies` _

locally_confluent :: A.Ix a => Relation a a -> Bit
locally_confluent r =
  let s = transitive_reflexive_closure r
  in  R.product (R.mirror r) r `R.implies` _

confluent :: A.Ix a => Relation a a -> Bit
confluent r =
  let s = transitive_reflexive_closure r
  in  _ s

terminating :: A.Ix a => Relation a a -> Bit
terminating r = _

main = do
  result <- solveWith minisat $ do
    r <- relation ((1,1),(4,4))
    assert $ and [ locally_confluent r
                 , not $ confluent r
                 ]
    return r
  case result of
    (Satisfied, Just r) -> do
      print r
      putStrLn $ table r