module Preds where

import Syntax hiding (lookUp)
import PrettyPrint

import TFFMonad
import TypesTerms


--------------------------------------------------------------------------------
-- Theorems
--

data Pred
    = Term := Term 
    | Pred :=> Pred 
    | Pred :/\ Pred 
    | Forall Term Pred              -- Term should be a Var term
        deriving (Eq,Show)

instance Printable Pred where
    ppi ((t1,_) := (t2,_))  = ppi t1 <+> text "=" <+> ppi t2
    ppi (p :=> q)           = wrap p <+> text "==>" <+> wrap q
    ppi (p :/\ q)           = wrap p <+> text "/\\" <+> wrap q
    ppi (Forall a p)        = text "!" <> ppTerm a <> text "."
                              $$ nest 4 (ppi p)


getRel :: Type -> Term -> Term -> FM Pred
getRel (Type ty) t1 t2
    = case ty of

        HsTyCon n -> return (t1 := t2)

        HsTyFun p q -> do
            { x  <- newVar (dom t1) 
            ; y  <- newVar (dom t2)
            ; r1 <- getRel p x y    
            ; r2 <- getRel q (applyTerm t1 x) (applyTerm t2 y)
            ; return $ Forall x $ Forall y $ r1 :=> r2
            } 


        HsTyVar a -> do
            { f <- lookUp a 
            ; return (t2 := applyTerm f t1)
            }


getRel (TyAll n t) t1 t2 = do
            { x <- newTVar
            ; y <- newTVar
            ; f <- newVar (mkTyFun x y)
            ; p <- inExtendedEnv n f $
                getRel t (applyType t1 x) (applyType t2 y)
            ; return (Forall f p)
            }
--
--------------------------------------------------------------------------------