PropPlogic

module PropPlogic where
import Prelude hiding (pred)
import PropPosSyntax(HsName,HsIdent,HsIdentI(..),HsExp,HsPat,HsQualType,hsPVar,
                     Assertion,Predicate,PredArg,PropOp,Quantifier)
import HasPropStruct
import MUtils
import Monad(mplus)

data Plogic
  = Quant Quantifier HsName (Maybe HsQualType) Plogic
  | App HsName [PredArg HsExp Plogic]
  | InfixApp Plogic HsName Plogic
  | Neg Plogic
  | Op PropOp Plogic Plogic
  | Equal HsExp HsExp
  | Has HsExp Plogic
  | Arrow Plogic Plogic
  | Lfp HsName Plogic
  | Gfp HsName Plogic
  | Nil
  | Lifted HsExp
  | Strong Plogic
  | Comp [(HsPat,Maybe HsQualType)] Plogic
  | Abs [HsIdent] Plogic
  | Paren Plogic -- preserve parens to rewrite infix apps after parsing

-- A hack to give '->' higher precedence than ':::' in Plogic assertions:
Has e p1 `arrow` p2 = Has e (p1 `Arrow` p2)
p1 `arrow` p2 = p1 `Arrow` p2

plogicAssertion p = prop p

prop :: (Functor m,Monad m) => Plogic -> m Assertion
prop p =
  case p of
    Quant q n optt p -> quant q n optt # prop p
    App n args -> propApp n # plogicArgs args
    Neg p -> propNeg # prop p
    Op op p1 p2 -> propOp op # prop p1 <# prop p2
    Equal e1 e2 -> return (propEqual e1 e2)
    Has e p -> propHas e # pred p
    Paren p -> propParen # prop p
    _ -> fail "Bad Plogic assertion" -- !!!

plogicArgs args = mapM plogicArg args
plogicArg args = either (return . Left) (Right #. pred) args

propDecl loc c xs p = uncurry (hsPropDecl loc c) # pred' xs p

pred' [] p = (,) [] # pred p
pred' args p = ((,) args # pred p) `mplus` pred'' args p
  where 
    pred'' args p =
      do HsVar x <- return (last args)
         (,) (init args) . predComp [(hsPVar x,Nothing)] # prop p

pred :: (Functor m,Monad m) => Plogic -> m Predicate
pred p =
  case p of
    App n args       -> predApp n # plogicArgs args
    Arrow p1 p2      -> predArrow # pred p1 <# pred p2
    InfixApp p1 i p2 -> predInfixApp # pred p1 <# return i <# pred p2
    Neg p            -> predNeg Nothing # pred p
    Op op p1 p2      -> predOp op Nothing # pred p1 <# pred p2
    Lfp i p          -> predLfp i # pred p
    Gfp i p          -> predGfp i # pred p
    Nil              -> return predNil
    Lifted e         -> return (predLifted e)
    Strong p         -> predStrong # pred p
    Comp tps p       -> predComp tps # prop p
    Abs is p         -> predAbs is # pred p
    Paren p          -> predParen # pred p
    _                -> fail "Bad Plogic predicate"