packages feed

Agda-2.3.2.2: src/prototyping/mixfix/Name.hs

------------------------------------------------------------------------
-- Names
------------------------------------------------------------------------

module Name
  ( Assoc(..)
  , Fixity(..)
  , fixAssocInvariant
  , ignoreAssoc
  , Name(..)
  , arity
  , isOperator
  , isOpenOperator
  , nameInvariant
  , pretty
  , string
  , name
  , operator
  , openOperator
  , tests
  ) where

import Data.Function
import qualified Data.Maybe as Maybe
import Control.Monad
import Test.QuickCheck
import qualified Data.List as List

import Utilities hiding (tests)

------------------------------------------------------------------------
-- Types

-- | Associativity.

data Assoc = Non | L | R
             deriving (Eq, Ord, Show)

-- | Fixity.

data Fixity = Prefix | Postfix | Infix
              deriving (Eq, Ord, Show)

-- | The associativity should always be 'Non' for non-infix operators.

fixAssocInvariant :: (Fixity, Assoc) -> Bool
fixAssocInvariant (Infix, _) = True
fixAssocInvariant (_, ass)   = ass == Non

-- | Ignores the associativity of non-infix operators.

ignoreAssoc :: Fixity -> Assoc -> (Fixity, Assoc)
ignoreAssoc Infix ass = (Infix, ass)
ignoreAssoc f     _   = (f,     Non)

prop_ignoreAssoc f a = fixAssocInvariant (ignoreAssoc f a)

-- | A name is a completely qualified name.

data Name = Name { moduleName :: [String]
                 , fixity     :: Maybe Fixity
                   -- ^ 'Just' something for operators.
                 , nameParts  :: [String]
                   -- ^ A /non-empty/ list of /non-empty/ name parts.
                   -- A singleton list for non-operators.
                 }
            deriving (Show, Eq, Ord)

-- | The arity of an operator (zero for non-operators).

arity :: Name -> Integer
arity n = List.genericLength (nameParts n) + case fixity n of
  Nothing      -> - 1
  Just Prefix  -> 0
  Just Postfix -> 0
  Just Infix   -> 1

-- | Is the name an operator?

isOperator :: Name -> Bool
isOperator = (> 0) . arity

-- | Is the name an open operator?

isOpenOperator :: Name -> Bool
isOpenOperator = Maybe.isJust . fixity

-- | The name invariant.

nameInvariant n@(Name m f ns) = nonEmpty ns && all nonEmpty ns
  where nonEmpty = not . null

-- | Pretty-prints a name.

pretty :: Name -> String
pretty n = List.intercalate "." (moduleName n ++ [name])
  where
  fixUp = case fixity n of
    Nothing      -> id
    Just Prefix  -> (++ "_")
    Just Postfix -> ("_" ++)
    Just Infix   -> ("_" ++) . (++ "_")
  name = fixUp (List.intercalate "_" $ nameParts n)

------------------------------------------------------------------------
-- Test data generators

instance Arbitrary Assoc where
  arbitrary = elements [Non, L, R]

instance Arbitrary Fixity where
  arbitrary = elements [Prefix, Postfix, Infix]

-- | Generates a string, of the given minimum and maximum lengths,
-- suitable for use in a name.

string :: Integer -- ^ Minimum length.
       -> Integer -- ^ Maximum length.
       -> Gen String
string min max = list (choose (min, max)) (elements "ab")

-- | Generates a name with the given fixity.

name :: Maybe Fixity -> Gen Name
name mfix = liftM3 Name mod (return mfix) op
  where
  character = elements "abcd"
  mod       = list (choose (0, 2 :: Integer)) $ string 1 1
  op        = list (choose (1, 3 :: Integer)) $ string 1 2

-- | Generates an open operator.

openOperator :: Gen Name
openOperator = name . Just =<< arbitrary

prop_openOperator =
  forAll openOperator $ \op ->
    isOpenOperator op

-- | Generates an operator.

operator :: Gen Name
operator = arbitrary `suchThat` isOperator

instance Arbitrary Name where
  arbitrary = name =<< arbitrary

  shrink (Name u f op) =
    filter nameInvariant $
    map (\(x, y, z) -> Name x y z) $
    shrink (u, f, op)

------------------------------------------------------------------------
-- Tests

-- | All tests.

tests = do
  quickCheck nameInvariant
  quickCheck (all nameInvariant . shrink)
  quickCheck prop_ignoreAssoc
  quickCheck prop_openOperator