------------------------------------------------------------------------
--- This module contains some operations to handle properties in
--- a Curry program.
---
--- @author Michael Hanus
--- @version December 2017
------------------------------------------------------------------------

module PropertyUsage
  ( isProperty, isPropType, isPropIOType, isEquivProperty
  , propModule, easyCheckModule, easyCheckExecModule
  )  where

import AbstractCurry.Types
import AbstractCurry.Select (funcType, resultType, funcRules)

------------------------------------------------------------------------
--- Check whether a function definition is a property,
--- i.e., if the result type is `Prop` or `PropIO`.
isProperty :: CFuncDecl -> Bool
isProperty = isPropertyType . funcType
 where
  isPropertyType ct = isPropIOType ct || isPropType (resultType ct)

--- Is the type expression the type Test.EasyCheck.Prop?
isPropType :: CTypeExpr -> Bool
isPropType texp = case texp of
  CTCons (mn,tc) [] -> tc == "Prop" && isCheckModule mn
  _                 -> False

--- Is the type expression the type Test.EasyCheck.PropIO?
isPropIOType :: CTypeExpr -> Bool
isPropIOType texp = case texp of
  CTCons (mn,tc) [] -> tc == "PropIO" && isCheckModule mn
  _                 -> False

--- Check whether a function definition is an equivalence property, i.e.,
--- has the form `test = f1 <=> f2`. If yes, returns both operations,
--- otherwise `Nothing` is returned.
isEquivProperty :: CFuncDecl -> Maybe (QName,QName)
isEquivProperty fdecl =
  case funcRules fdecl of
    [CRule []
      (CSimpleRhs (CApply (CApply (CSymbol prop) (CSymbol f1)) (CSymbol f2)) [])] -> if isEquivSymbol prop then Just (f1,f2) else Nothing
    _ -> Nothing
 where
  isEquivSymbol (qn,mn) = isCheckModule qn && mn=="<=>"

-- Is the module name Test.Prop or Test.EasyCheck?
isCheckModule :: String -> Bool
isCheckModule mn = mn == propModule || mn == easyCheckModule

--- Name of the Test.Prop module (the clone of the EasyCheck module).
propModule :: String
propModule = "Test.Prop" 

--- Name of the EasyCheck module.
easyCheckModule :: String
easyCheckModule = "Test.EasyCheck" 

--- Name of the EasyCheckExec module.
easyCheckExecModule :: String
easyCheckExecModule = "Test.EasyCheckExec"