module clausal (Const Func Var Pred : Set)  where
open import Data.List hiding (all ; and ; or )
open import Data.Bool hiding ( not )
open import Function

open import Logic Const Func Var Pred 

-- data Expr  : Set  where
--    var   : Var → Expr 
--    func  : Func → Expr → Expr 
--    const : Const → Expr 
--    _,_ : Expr →Expr → Expr 

-- data Statement : Set where
--    pred       : Pred  → Statement 
--    predx  : Pred  → Expr → Statement 
--    _/\_   : Statement → Statement  → Statement 
--    _\/_         : Statement → Statement  → Statement 
--    ¬_         : Statement  → Statement 
--    All_=>_        : Var → Statement → Statement 
--    Exist_=>_      : Var → Statement → Statement 

-- make negations on predicates only
negin1  : Statement → Statement

negin  : Statement → Statement
negin (pred x) = pred x
negin (predx x x₁) = predx x x₁
negin (s /\ s₁) = negin s /\ negin s₁
negin (s \/ s₁) = negin s \/ negin s₁
negin (¬ s) = negin1 s
negin (All x => s) = All x => negin s
negin (Exist x => s) = Exist x => negin s

negin1 (pred x) = ¬ (pred x)
negin1 (predx x x₁) = ¬ (predx x x₁)
negin1 (s /\ s₁) = negin1 s \/ negin1 s₁
negin1 (s \/ s₁) = negin1 s /\ negin1 s₁
negin1 (¬ s) = negin s
negin1 (All x => s) = (Exist x => negin1 s )
negin1 (Exist x => s) = (All x => negin1 s)

-- remove existential quantifiers using sokem functions
--    enough unused functions and constants for skolemization necessary
--    assuming non overrupping quantified variables

record Skolem : Set where
   field 
     st : Statement
     cl : List Const
     fl : List Func
     vr : List Var

{-# TERMINATING #-} 
skolem  : List Const → List Func → (sbst : Expr  → Var →  Expr  → Expr  ) → Statement → Statement
skolem cl fl sbst s = Skolem.st (skolemv record { st = s ; cl = cl ; fl = fl ; vr = [] })  where
   skolemv : Skolem → Skolem
   skolemv S with Skolem.vr S | Skolem.st S 
   skolemv S | v | All x => s  = record S1 { st = All x => Skolem.st S1 } where
        S1 : Skolem 
        S1 = skolemv record S { st = s ;  vr = x ∷ v } 
   skolemv S | [] | (Exist x => s) with Skolem.cl S
   ... | [] = S
   ... | sk ∷ cl = skolemv record S { st = subst-prop s sbst x (Expr.const sk) ; cl = cl }
   skolemv S | (v ∷ t) | (Exist x => s)  with Skolem.fl S
   ... | [] = S
   ... | sk ∷ fl = skolemv record S { st = subst-prop s sbst x (func sk (mkarg v t )) ; fl = fl }  where
      mkarg : (v : Var) (vl : List Var ) → Expr
      mkarg v []  = var v
      mkarg v (v1 ∷ t )  = var v , mkarg v1 t
   skolemv S | v | s /\ s₁ = record S2 { st = Skolem.st S1 /\ Skolem.st S2 }  where
        S1 = skolemv record S {st = s}
        S2 = skolemv record S1 {st = s₁}
   skolemv S | v | s \/ s₁ = record S2 { st = Skolem.st S1 \/ Skolem.st S2 }  where
        S1 = skolemv record S {st = s}
        S2 = skolemv record S1 {st = s₁}
   skolemv S | _ | _ = S

-- remove universal quantifiers
univout  : Statement → Statement
univout (s /\ s₁) = univout s /\ univout s₁
univout (s \/ s₁) = univout s \/ univout s₁
univout x = x

-- move disjunctions inside
{-# TERMINATING #-} 
conjn1  : Statement → Statement

{-# TERMINATING #-} 
conjn  : Statement → Statement
conjn (s /\ s₁) = conjn s /\ conjn s₁
conjn (s \/ s₁) = conjn1 ( ( conjn s ) \/ ( conjn s₁) )
conjn x = x

conjn1 ((x /\ y) \/ z) = conjn (x \/ y) /\ conjn (x \/ z )
conjn1 (z \/ (x /\ y)) = conjn (z \/ x) /\ conjn (z \/ y )
conjn1 x = x

data Clause  : Set where
   _:-_ : ( x y : List Statement ) → Clause

-- turn into [ [  [ positive ] :- [ negative ] ]
--   to remove overraps, we need equality
clausify : Statement → List Clause
clausify s = clausify1 s [] where
   inclause : Statement → Clause → Clause
   inclause (x \/ y ) a  = inclause x ( inclause y a ) 
   inclause (¬ x) (a :- b )  = a :- ( x ∷ b ) 
   inclause  x (a :- b)   = ( x ∷ a ) :- b  
   clausify1 : Statement → List Clause → List Clause
   clausify1 (x /\ y) c =  clausify1 y (clausify1 x c )
   clausify1 x c = inclause x ([] :- [] ) ∷ c

translate : Statement → List Const → List Func  →  (sbst : Expr  → Var →  Expr  → Expr  ) →  List Clause
translate s cl fl sbst = clausify $ conjn $ univout $ skolem cl fl sbst $ negin s