--  Copyright (C) 2006-2008 Angelos Charalambidis <a.charalambidis@di.uoa.gr>
--
--  This program is free software; you can redistribute it and/or modify
--  it under the terms of the GNU General Public License as published by
--  the Free Software Foundation; either version 2, or (at your option)
--  any later version.
--
--  This program is distributed in the hope that it will be useful,
--  but WITHOUT ANY WARRANTY; without even the implied warranty of
--  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--  GNU General Public License for more details.
--
--  You should have received a copy of the GNU General Public License
--  along with this program; see the file COPYING.  If not, write to
--  the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
--  Boston, MA 02110-1301, USA.

-- | Higher Order Predicate Language
module Hopl where

import Lang
import Types
import Data.Monoid

data Expr a =
       App (Expr a) (Expr a)
    |  Flex a
    |  Rigid a
    |  Lambda a (Expr a)
  deriving (Eq, Show)

data Clause a = C a (Expr a) deriving Eq

isFlex (Flex _) = True
isFlex _ = False

isRigid (Rigid _) = True
isRigid _ = False

clauseHead (C a _) = a
clauseBody (C _ b) = b

type Goal a = Expr a

instance (Symbol a, Eq a)  => HasLogicConstants (Expr a) where
    ctop    = Rigid $ liftSym "true"
    cbot    = Rigid $ liftSym "false"
    ceq     = Rigid $ liftSym "="
    cexists = Rigid $ liftSym "_exists"
    cor     = Rigid $ liftSym ";"
    cand    = Rigid $ liftSym ","

{-
instance (HasConstants a, HasType a) => HasConstants (Typed a) where
    ctop = typed tyBool ctop
    cbot = typed tyBool cbot
    ceq = typed (TyFun tyAll tyAll) ceq
    cexists = typed (TyFun (TyVar undefined) tyBool) cexists
    cor = typed (TyFun tyBool ((TyFun tyBool) tyBool)) cor
    cand = typed (TyFun tyBool ((TyFun tyBool) tyBool)) cand
-}
{-
instance (Eq a, Symbol a) => HasConstants (Expr (Typed a)) where
    ctop = Const (typed tyBool (liftSym "1"))
    cbot = Const (typed tyBool (liftSym "0"))
    ceq  = Const (typed (TyFun tyAll tyAll) (liftSym "="))
    cexists = Const (typed (TyFun (TyVar undefined) tyBool) (liftSym "exists"))
    cor = Const (typed (TyFun tyBool ((TyFun tyBool) tyBool)) (liftSym "or"))
    cand = Const (typed (TyFun tyBool ((TyFun tyBool) tyBool)) (liftSym "and"))
    isEqual(Const (T s _)) = s == liftSym "="
    isConj (Const (T s _)) = s == liftSym "and"
    isDisj (Const (T  s _)) = s == liftSym "or"
    isTop (Const (T s _)) = s == liftSym "1"
    isBot (Const (T s _)) = s == liftSym "0"
    isExistsQ (Const (T s _)) = s == liftSym "exists"
-}

contradiction :: HasLogicConstants a => a
contradiction = ctop

isContra :: HasLogicConstants a => a -> Bool
isContra = (==contradiction)

instance Symbol a => HasSignature (Expr a) a where
	sig (App e1 e2) = sig e1 `mappend` sig e2
	sig (Flex a)  = varSig a
	sig (Rigid a) = rigSig a
        sig (Lambda a x) = varSig a `mappend` sig x

instance Symbol a => HasSignature (Clause a) a where
	sig (C p e2) = rigSig p `mappend` sig e2 `mappend` mempty

--instance HasSignature (Goal a) a where
--	sig gs = mconcat $ map sig gs

instance (Symbol a, Eq a, HasType a) => HasType (Expr a) where
	typeOf (App e1 e2) =
            case typeOf e1 of
                (TyFun a b) -> b
                t -> error ("not expected type " ++ (show t))
	typeOf (Flex a)  = typeOf a
        typeOf c@(Rigid a)
            | c == ctop = tyBool
            | c == cbot = tyBool
            | c == cor  = TyFun tyBool ((TyFun tyBool) tyBool)
            | c == cand = TyFun tyBool ((TyFun tyBool) tyBool)
            | c == ceq  = TyFun tyAll ((TyFun tyAll) tyBool)
            | c == cexists = TyFun (TyVar undefined) tyBool
            | otherwise = typeOf a
	typeOf (Lambda a e) =
            let t = typeOf e
                t1 = typeOf a
            in TyFun t1 t
        hasType ty e = error "hasType"

instance HasType a => HasType (Clause a) where
	typeOf c = liftGround TyBool
        hasType ty c =
            if not (ty == tyBool) then
                error "clause can have not boolean type"
            else c

-- instance HasType a => HasType (Goal a) where
--	typeOf g = liftGround TyBool

-- liftSet :: Expr a -> Expr a
-- liftSet e@(Set _ _) = e
-- liftSet (Flex v) = Set [] [v]
-- liftSet _ = error ("Cannot represent expression as set")

functor :: Expr a -> Expr a
functor (App e a) = functor e
functor e = e

args (App e a) = args2 e ++ [a]
    where args2 (App e a) = args2 e ++ [a]
          args2 e = []