free-theorems (empty) → 0.2

raw patch · 33 files changed

+6609/−0 lines, 33 filesdep +basedep +containersdep +haskell-srcsetup-changed

Dependencies added: base, containers, haskell-src, haskell-src-exts, mtl, pretty

Files

• LICENSE +4/−0
• README +57/−0
• Setup.lhs +4/−0
• free-theorems.cabal +51/−0
• runtests +3/−0
• src/Arbitraries.hs +195/−0
• src/FrontendCheckGlobalTests.hs +188/−0
• src/FrontendCheckLocalTests.hs +425/−0
• src/FrontendOtherTests.hs +77/−0
• src/FrontendTypeExpressionsTests.hs +314/−0
• src/InterpretationTests.hs +100/−0
• src/Language/Haskell/FreeTheorems.hs +197/−0
• src/Language/Haskell/FreeTheorems/BasicSyntax.hs +256/−0
• src/Language/Haskell/FreeTheorems/Frontend.hs +136/−0
• src/Language/Haskell/FreeTheorems/Frontend/CheckGlobal.hs +418/−0
• src/Language/Haskell/FreeTheorems/Frontend/CheckLocal.hs +397/−0
• src/Language/Haskell/FreeTheorems/Frontend/Error.hs +130/−0
• src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs +302/−0
• src/Language/Haskell/FreeTheorems/Intermediate.hs +408/−0
• src/Language/Haskell/FreeTheorems/LanguageSubsets.hs +59/−0
• src/Language/Haskell/FreeTheorems/NameStores.hs +65/−0
• src/Language/Haskell/FreeTheorems/Parser/Haskell98.hs +472/−0
• src/Language/Haskell/FreeTheorems/Parser/Hsx.hs +528/−0
• src/Language/Haskell/FreeTheorems/PrettyBase.hs +58/−0
• src/Language/Haskell/FreeTheorems/PrettyTheorems.hs +464/−0
• src/Language/Haskell/FreeTheorems/PrettyTypes.hs +285/−0
• src/Language/Haskell/FreeTheorems/Syntax.hs +54/−0
• src/Language/Haskell/FreeTheorems/Theorems.hs +230/−0
• src/Language/Haskell/FreeTheorems/Unfold.hs +521/−0
• src/Language/Haskell/FreeTheorems/ValidSyntax.hs +52/−0
• src/ParserPrettyPrinterTests.hs +100/−0
• src/Runtests.hs +21/−0
• src/Tests.hs +38/−0

@@ -0,0 +1,4 @@+This software is in the public domain.  Permission to use,  copy, modify,  and+distribute this software and its documentation for any purpose and without fee+is hereby granted,  without any conditions or restrictions.   This software is+provided "as is" without expressed or implied warranty.

@@ -0,0 +1,57 @@++  DESCRIPTION++This library may be used to automatically generate free theorems+[1,2] from Haskell type signatures. It supports Haskell 98 and +additionally higher-rank functions. Beside primitive Haskell types+(Int, Integer, Float, Double, Char), it already includes lists and+tuples. The library provides means to add other data types.++++  DEPENDENCIES++See the file `free-theorems.cabal' for dependencies. Note that there,+two parser libraries are listed. If only one is needed, the library+is easily adjustable by commenting out the corresponding dependencies+and exported modules.+++  +  INSTALL++Since this library is cabalised, it uses the standard installation+process.+  +  runhaskell Setup.lhs configure+  runhaskell Setup.lhs build+  runhaskell Setup.lhs install++++  USAGE++See the Haddock-generated documentation for detailed information on+how to use this library.++++  DOCUMENTATION++If Haddock is available, documentation may be +generated automatically from the sources.+  +  runhaskell Setup.lhs haddock++++-------++[1] Philip Wadler, Theorems for free!, In Functional Programming+    Languages and Computer Architecture, Proceedings, 1989.++[2] Patricia Johann and Janis Voigtländer, The Impact of seq on Free+    Theorems-Based Program Transformations, In Fundamenta +    Informaticae, 2006.++

@@ -0,0 +1,4 @@+#!/usr/bin/env runhaskell+ +> import Distribution.Simple+> main = defaultMain

@@ -0,0 +1,51 @@+name:           free-theorems+version:        0.2+license:        PublicDomain+license-file:   LICENSE+author:         Sascha Boehme+maintainer:     voigt@tcs.inf.tu-dresden.de+synopsis:       Automatic generation of free theorems.+description:+    The free-theorems library allows to automatically generate free+    theorems from Haskell type expressions. It supports nearly all+    Haskell 98 types except of type constructor classes, and in+    addition it can also handle higher-rank functions. Free theorems+    are generated for three different sublanguages of Haskell, a+    basic one corresponding to the polymorphic lambda-calculus of +    Girard-Reynolds, an extension of that allowing for recursion and+    errors, and finally a sublanguage additionally allowing seq.+    In the last two sublanguages, also inequational free theorems+    may be derived in addition to classical equational results.+category:       Language+tested-with: 	GHC==6.8.2+build-type:	Simple+build-depends:+    base >= 1.0+  , mtl >= 1.0+  , haskell-src >= 1.0+  , haskell-src-exts >= 0.2.1+  , pretty >= 1.0.0.0+  , containers >= 0.1.0.1+exposed-modules:+    Language.Haskell.FreeTheorems+    Language.Haskell.FreeTheorems.Syntax+    Language.Haskell.FreeTheorems.Parser.Haskell98+    Language.Haskell.FreeTheorems.Parser.Hsx+    Language.Haskell.FreeTheorems.Theorems+other-modules:+    Language.Haskell.FreeTheorems.BasicSyntax+    Language.Haskell.FreeTheorems.ValidSyntax+    Language.Haskell.FreeTheorems.NameStores+    Language.Haskell.FreeTheorems.Frontend+    Language.Haskell.FreeTheorems.Frontend.Error+    Language.Haskell.FreeTheorems.Frontend.TypeExpressions+    Language.Haskell.FreeTheorems.Frontend.CheckLocal+    Language.Haskell.FreeTheorems.Frontend.CheckGlobal+    Language.Haskell.FreeTheorems.LanguageSubsets+    Language.Haskell.FreeTheorems.Intermediate+    Language.Haskell.FreeTheorems.Unfold+    Language.Haskell.FreeTheorems.PrettyBase+    Language.Haskell.FreeTheorems.PrettyTypes+    Language.Haskell.FreeTheorems.PrettyTheorems+hs-source-dirs: src+extensions:     Generics, DeriveDataTypeable, Rank2Types, PatternSignatures

@@ -0,0 +1,3 @@+#!/bin/bash++runhaskell -isrc -fglasgow-exts src/Runtests.hs

@@ -0,0 +1,195 @@++++-- | Gives instance of the class Arbitrary for several data types of the+--   library. These instances are needed by QuickCheck.+--   See also "Tests".++module Arbitraries where++++import Control.Monad+import Data.Generics (Typeable, Data)+import Test.QuickCheck++import Language.Haskell.FreeTheorems.Syntax+import Language.Haskell.FreeTheorems.LanguageSubsets++++newtype ListOfDeclarations = ListOfDeclarations +  { getDeclarations :: [Declaration] }+  deriving (Eq, Show)++instance Arbitrary ListOfDeclarations where+  arbitrary = do n <- choose (1, 100)+                 liftM ListOfDeclarations (replicateM n arbitrary)+  coarbitrary _ = id++++instance Arbitrary Declaration where+  arbitrary = oneof [ liftM DataDecl arbitrary+                    , liftM NewtypeDecl arbitrary+                    , liftM TypeDecl arbitrary+                    , liftM ClassDecl arbitrary+                    , liftM TypeSig arbitrary ]+  coarbitrary _ = id++++instance Arbitrary DataDeclaration where+  arbitrary = do n <- arbIdent id 'T'+                        [ "Bool", "Maybe", "Either", "Ordering" ]+                 v <- choose (0, 5)+                 c <- choose (1, 7)+                 liftM2 (Data n) (replicateM v arbitrary) +                                 (replicateM c arbitrary)+  coarbitrary _ = id++++instance Arbitrary NewtypeDeclaration where+  arbitrary = do n <- arbIdent id 'T' []+                 v <- choose (0, 5)+                 c <- arbIdent id 'D' []+                 liftM2 (\vs -> Newtype n vs c)+                        (replicateM v arbitrary) arbitrary+  coarbitrary _ = id++++instance Arbitrary TypeDeclaration where+  arbitrary = do n <- arbIdent id 'T'+                        [ "String", "Ordering", "Rational", "ShowS", "ReadS"+                        , "FilePath" ]+                 v <- choose (0, 5)+                 liftM2 (Type n) (replicateM v arbitrary) arbitrary+  coarbitrary _ = id++++instance Arbitrary ClassDeclaration where+  arbitrary = do c <- choose (0, 3)+                 p <- replicateM c (arbitrary :: Gen TypeClass)+                 n <- arbIdent id 'C'+                        [ "Eq", "Ord", "Num", "Integral", "Show", "Read"+                        , "Bounded", "Enum", "Real", "Fractional", "Floating"+                        , "RealFrac", "RealFloat" ]+                 s <- choose (0, 10)+                 liftM2 (Class p n) arbitrary (replicateM s arbitrary)+  coarbitrary _ = id++++instance Arbitrary Signature where+  arbitrary = do s <- arbIdent id 'f'+                        [ "not", "(&&)", "(||)", "(==)", "(/=)", "maybe"+                        , "either", "fst", "snd", "curry", "uncurry", "(<)"+                        , "(>)", "max", "min", "succ", "pred", "(+)", "(-)"+                        , "div", "mod", "pi", "id", "flip", "const", "map"+                        , "filter", "head", "tail", "length", "foldr", "foldl" ]+                 liftM (Signature s) arbitrary+  coarbitrary _ = id++++instance Arbitrary DataConstructorDeclaration where+  arbitrary = do con <- arbIdent id 'D'+                            [ "False", "True", "Left", "Right", "Nothing"+                            , "Just", "LT", "GT", "EQ" ]+                 i <- choose (0, 5)+                 liftM (DataCon con) (replicateM i arbitrary)+  coarbitrary _ = id++++instance Arbitrary BangTypeExpression where+  arbitrary = oneof [ liftM Banged arbitrary, liftM Unbanged arbitrary ]+  coarbitrary _ = id++++instance Arbitrary TypeExpression where+  arbitrary = sized arbTypeExpr+  coarbitrary _ = id++arbTypeExpr n =+  if n == 0+    then oneof [ liftM TypeVar arbitrary+               , liftM (\c -> TypeCon c []) arbitrary+               , liftM TypeExp arbitrary ]+    else frequency [ (1, arbTypeExpr 0)+                   , (2, arbComplexTypeExpr (n `div` 2))+                   ]++arbComplexTypeExpr n = oneof+  [ do r <- choose (1, 7)+       liftM2 TypeCon arbitrary (replicateM r (arbTypeExpr n))+  , liftM2 TypeFun (arbTypeExpr n) (arbTypeExpr n)+  , do c <- choose (0, 2)+       liftM3 TypeAbs arbitrary (replicateM c arbitrary) (arbTypeExpr n)+  ]++++instance Arbitrary TypeConstructor where+  arbitrary = oneof+                [ oneof +                    [ return ConUnit+                    , return ConList+                    , do n <- choose (2, 15)+                         return (ConTuple n)+                    , return ConInt+                    , return ConInteger+                    , return ConFloat+                    , return ConDouble+                    , return ConChar+                    ]+                , arbIdent Con 'T' +                    [ "Bool", "Maybe", "Either", "String", "Ordering"+                    , "Rational", "ShowS", "ReadS", "FilePath" ]+                ]+  coarbitrary _ = id++++instance Arbitrary TypeVariable where+  arbitrary = arbIdent TV 'a' ["a", "b", "c", "d", "e"]+  coarbitrary _ = id++++instance Arbitrary TypeClass where+  arbitrary = arbIdent TC 'C'+                [ "Eq", "Ord", "Num", "Integral", "Show", "Read", "Bounded"+                , "Enum", "Real", "Fractional", "Floating", "RealFrac"+                , "RealFloat" ]+  coarbitrary _ = id++++instance Arbitrary FixedTypeExpression where+  arbitrary = oneof (map (return . TF . Ident) [ "t1", "t2", "t3", "t4", "t5" ])+  coarbitrary _ = id++++instance Arbitrary LanguageSubset where+  arbitrary = oneof+    [ return $ BasicSubset+    , return $ SubsetWithFix EquationalTheorem+    , return $ SubsetWithFix InequationalTheorem+    , return $ SubsetWithSeq EquationalTheorem+    , return $ SubsetWithSeq InequationalTheorem+    ]+  coarbitrary _ = id++++arbIdent :: (Identifier -> a) -> Char -> [String] -> Gen a+arbIdent f c xs =+  oneof . map (return . f . Ident) $ xs ++ map (\i -> c : show i) [1..20]++

@@ -0,0 +1,188 @@++++module FrontendCheckGlobalTests (tests) where++++import Control.Monad.Writer (runWriter)+import Data.Generics (everything, mkQ)+import Data.List (nub, find)+import Data.Maybe (mapMaybe, catMaybes)+import Data.Set as Set (isSubsetOf, union, empty, singleton, fromList)+import Test.QuickCheck++import Tests+import Language.Haskell.FreeTheorems.Syntax+import Language.Haskell.FreeTheorems.Frontend as FT +import Language.Haskell.FreeTheorems.Frontend.CheckGlobal+++++-- | Runs all tests.++tests :: IO ()+tests = do+  doTest "check global at most one declaration per name"+    prop_checkGlobalAtMostOneDeclPerName+  doTest "check global arities match" prop_checkGlobalAritiesMatch+  doTest "check global type class hierarchy acyclic"+    prop_checkGlobalAcyclicTypeClasses+  doTest "check global type synonyms not mutually recursive"+    prop_checkGlobalTypeSynonymsNotMutuallyRecursive+  doTest "check global only declared classes occur"+    prop_checkGlobalTypeClasses    +  doTest "check global only declared constructors occur"+    prop_checkGlobalConstructors++++++-- | Property: Check that there are no duplicate declarations by comparing the +--   names of the declarations.++prop_checkGlobalAtMostOneDeclPerName ds0 =+  checkDecls ds0 $ \ds ->+    let names = map getDeclarationName ds+     in length (nub names) == length names++++-- | Property: Checks that every type constructor is used with the arity it was+--   declared with. If any occurring type constructor is not declared, no arity+--   check is performed for it.++prop_checkGlobalAritiesMatch ds0 =+  checkDecls ds0 $ \ds ->+    everything (&&) (True `mkQ` checkArity ds) ds+    +checkArity ds t = case t of+  TypeCon con ts -> correctArity ds con (length ts)+  otherwise      -> True++correctArity ds con arity = case con of+  ConUnit    -> arity == 0+  ConList    -> arity == 1+  ConTuple n -> arity == n+  ConInt     -> arity == 0+  ConInteger -> arity == 0+  ConFloat   -> arity == 0+  ConDouble  -> arity == 0+  ConChar    -> arity == 0+  Con c      -> maybe True (== arity) (getArityFromDecl ds c)++getArityFromDecl ds c =+  case find (\d -> getDeclarationName d == c) ds of+    Just (DataDecl d)    -> Just . length . dataVars $ d+    Just (NewtypeDecl d) -> Just . length . newtypeVars $ d+    Just (TypeDecl d)    -> Just . length . typeVars $ d+    otherwise            -> Nothing++++-- | Property: Checks that the type class hierarchy is acyclic.++prop_checkGlobalAcyclicTypeClasses ds0 =+  checkDecls ds0 $ \ds ->+    hasCycle classDeps ds++classDeps d = case d of+  ClassDecl d -> map (\(TC c) -> c) (superClasses d)+  otherwise   -> []++++-- | Property: Checks that type synonyms are not mutually recursively declared.++prop_checkGlobalTypeSynonymsNotMutuallyRecursive ds0 =+  checkDecls ds0 $ \ds ->+    hasCycle (typeDeps (mapMaybe getTypeSynName ds)) ds++getTypeSynName d = case d of+  TypeDecl d -> Just (typeName d)+  otherwise  -> Nothing++typeDeps ds = everything (++) ([] `mkQ` getTypeCon)+  where+    getTypeCon t = case t of+      TypeCon (Con c) _ -> if c `elem` ds then [c] else []+      otherwise         -> []++++-- | Property: Check that every occurring type class is declared.++prop_checkGlobalTypeClasses ds0 =+  checkDecls ds0 $ \ds ->+    occurringClasses ds `Set.isSubsetOf` declaredClasses ds+  +occurringClasses = everything Set.union (Set.empty `mkQ` occurring)+  where+    occurring (TC c) = Set.singleton c++declaredClasses = Set.fromList . mapMaybe getClassName+  where+    getClassName d = case d of+      ClassDecl d -> Just (className d)+      otherwise   -> Nothing++++-- | Property: Check that every occurring type constructor is declared.++prop_checkGlobalConstructors ds0 =+  checkDecls ds0 $ \ds ->+    occurringCons ds `Set.isSubsetOf` declaredCons ds++occurringCons = everything Set.union (Set.empty `mkQ` occurring)+  where+    occurring con = case con of+      Con c     -> Set.singleton c+      otherwise -> Set.empty++declaredCons = Set.fromList . mapMaybe getConName+  where+    getConName d = case d of+      DataDecl d    -> Just (dataName d)+      NewtypeDecl d -> Just (newtypeName d)+      TypeDecl d    -> Just (typeName d)+      otherwise     -> Nothing++++++++-- | Runs a property on to list of declarations. The first list is checked+--   and then fed to 'checkGlobal' along with the second list. The result+--   and the first (checked) list are then given to the property.++checkDecls :: ListOfDeclarations -> ([Declaration] -> Bool) -> Property+checkDecls ds prop =+  let ds' = fst . runWriter . checkGlobal [] . getDeclarations $ ds+   in not (null ds') ==> prop ds'+        +++-- | Checks if the given list of declarations has any cycles. The test is based+--   on the provided function which computes the dependencies of a declaration.++hasCycle :: (Declaration -> [Identifier]) -> [Declaration] -> Bool+hasCycle deps ds = +  any (\d -> cycle (length ds) d d) ds+  where+    cycle i d1 d2 =+      if i == 0+        then False+        else null (deps d2)+             || getDeclarationName d1 `elem` deps d2+             || any (cycle (i-1) d1) (declsDependingOn d2)++    declsDependingOn d =+      filter (\d' -> getDeclarationName d' `elem` deps d) ds+++

@@ -0,0 +1,425 @@++++module FrontendCheckLocalTests (tests) where++++import Control.Monad.Writer (runWriter)+import Data.Generics (Typeable, Data, everything, mkQ)+import Data.List (nub)+import Data.Maybe (fromJust, isJust, mapMaybe)+import Data.Set as Set+    (Set, empty, union, fromList, isSubsetOf, member, singleton)+import Test.QuickCheck++import Tests++import Language.Haskell.FreeTheorems.Syntax+import Language.Haskell.FreeTheorems.Frontend+import Language.Haskell.FreeTheorems.Frontend.Error+import Language.Haskell.FreeTheorems.Frontend.TypeExpressions+import Language.Haskell.FreeTheorems.Frontend.CheckLocal+import Language.Haskell.FreeTheorems.Frontend.CheckGlobal++++-- | Runs all tests.++tests :: IO ()+tests = do++  doTest "check local data free variables" prop_checkLocalDataFreeVars+  doTest "check local data distinct variables" prop_checkLocalDataVars+  doTest "check local data not primitive" prop_checkLocalDataNotPrim+  doTest "check local data no fixed types" prop_checkLocalDataNoFixedTEs+  doTest "check local data has data constructor" prop_checkLocalDataNotEmpty+  doTest "check local data not nested" prop_checkLocalDataNotNested+  doTest "check local data no function nor abstraction"+    prop_checkLocalDataAbsFun++  doTest "check local newtype free variables" prop_checkLocalNewtypeFreeVars+  doTest "check local newtype distinct variables" prop_checkLocalNewtypeVars+  doTest "check local newtype not primitive" prop_checkLocalNewtypeNotPrim+  doTest "check local newtype no fixed types" prop_checkLocalNewtypeNoFixedTEs+  doTest "check local newtype not nested" prop_checkLocalNewtypeNotNested+  doTest "check local newtype no function nor abstraction"+    prop_checkLocalNewtypeAbsFun++  doTest "check local type free variables" prop_checkLocalTypeFreeVars+  doTest "check local type distinct variables" prop_checkLocalTypeVars+  doTest "check local type not primitive" prop_checkLocalTypeNotPrim+  doTest "check local type no fixed types" prop_checkLocalTypeNoFixedTEs+  doTest "check local type not nested" prop_checkLocalTypeNotNested++  doTest "check local class methods distinct"+    prop_checkLocalClassMethodsDistinct+  doTest "check local class variable is free in methods"+    prop_checkLocalClassFreeVar+  doTest "check local class not recursive" prop_checkLocalClassNotRecursive+  doTest "check local class not primitive" prop_checkLocalClassNotPrim+  doTest "check local class no fixed types" prop_checkLocalClassNoFixedTEs++  doTest "check local signature no fixed types"+    prop_checkLocalSignatureNoFixedTEs++   +++++------- Test local checks -----------------------------------------------------+++-- | Property: Checks in data declarations that free variables of the right-hand+--   side are declared on the left-hand side.++prop_checkLocalDataFreeVars d = +  checkInData d $ \d' ->+    allFreeVars (dataCons d') `Set.isSubsetOf` Set.fromList (dataVars d')+  where+    allFreeVars :: (Typeable a, Data a) => a -> Set.Set TypeVariable+    allFreeVars = everything (Set.union) (Set.empty `mkQ` freeVars)++    freeVars :: BangTypeExpression -> Set.Set TypeVariable+    freeVars = freeTypeVariables . withoutBang++++-- | Property: Checks in data declarations that the left-hand side variables are+--   pairwise distinct.++prop_checkLocalDataVars d =+  checkInData d $ \d' ->+    length (nub (dataVars d')) == length (dataVars d')++++-- | Property: Checks in data declarations that the declared type constructor is+--   not a primitive type.++prop_checkLocalDataNotPrim d =+  checkInData d $ \d' ->+    isNotPrimitive (dataName d')++++-- | Property: Checks in data declarations that no FixedTypeExpression occurs+--   anywhere.++prop_checkLocalDataNoFixedTEs d =+  checkInData d $ \d' ->+    not (hasFixedTypeExpressions d')++++-- | Property: Checks that data declarations have at least one data constructor.++prop_checkLocalDataNotEmpty d =+  checkInData d $ \d' ->+    not (null (dataCons d'))++++-- | Property: Checks that data declarations are not nested.++prop_checkLocalDataNotNested d =+  checkInData d $ \d' ->+    not (isNested (dataName d') (dataCons d'))++++-- | Property: Checks in newtype declarations that variables of the right-hand+--   side are declared on the left-hand side.++prop_checkLocalNewtypeFreeVars d =+  checkInNewtype d $ \d' ->+    freeTypeVariables (newtypeRhs d') +        `Set.isSubsetOf` Set.fromList (newtypeVars d')++++-- | Property: Checks in newtype declarations that left-hand side variables+--   are pairwise distinct.++prop_checkLocalNewtypeVars d =+  checkInNewtype d $ \d' ->+    length (nub (newtypeVars d')) == length (newtypeVars d')++++-- | Property: Checks in newtype declarations that the declared type constructor+--   is not equal to the name of a primitive type.++prop_checkLocalNewtypeNotPrim d =+  checkInNewtype d $ \d' ->+    isNotPrimitive (newtypeName d')++++-- | Property: Checks in newtype declarations that no FixedTypeExpression +--   occurs.++prop_checkLocalNewtypeNoFixedTEs d =+  checkInNewtype d $ \d' ->+    not (hasFixedTypeExpressions d')++++-- | Property: Checks that newtype declarations are not nested.++prop_checkLocalNewtypeNotNested d =+  checkInNewtype d $ \d' ->+    not (isNested (newtypeName d') (newtypeRhs d'))++++-- | Property: Checks in type declarations that variables of the right-hand+--   side are declared on the left-hand side.++prop_checkLocalTypeFreeVars d =+  checkInType d $ \d' ->+    freeTypeVariables (typeRhs d') `Set.isSubsetOf` Set.fromList (typeVars d')++++-- | Property: Checks in type declarations that left-hand side variables+--   are pairwise distinct.++prop_checkLocalTypeVars d =+  checkInType d $ \d' ->+    length (nub (typeVars d')) == length (typeVars d')++++-- | Property: Checks in type declarations that the declared type constructor+--   is not equal to the name of a primitive type.++prop_checkLocalTypeNotPrim d =+  checkInType d $ \d' ->+    isNotPrimitive (typeName d')++++-- | Property: Checks in type declarations that no FixedTypeExpression +--   occurs.++prop_checkLocalTypeNoFixedTEs d =+  checkInType d $ \d' ->+    not (hasFixedTypeExpressions d')++++-- | Property: Checks that type declarations are not recursive.++prop_checkLocalTypeNotNested d =+  checkInType d $ \d' ->+    not (isRecursive (typeName d') (typeRhs d'))++++-- | Property: Checks in class declarations that the class methods have pairwise+--   distinct names.++prop_checkLocalClassMethodsDistinct d =+  checkInClass d $ \d' ->+    let methodNames = map signatureName (classFuns d')+     in length (nub methodNames) == length methodNames++++-- | Property: Checks in class declarations that the class variable occurs free+--   in all class method types.++prop_checkLocalClassFreeVar d =+  checkInClass d $ \d' ->+    let set = Set.singleton (classVar d')+     in all (\t -> (classVar d') `Set.member` freeTypeVariables t)+            (map signatureType (classFuns d'))++++-- | Property: Checks in class declarations that the class name does not occur+--   in a type expression of any class method.++prop_checkLocalClassNotRecursive d =+  checkInClass d $ \d' ->+    not (isRecursive (className d') (classFuns d'))    ++++-- | Property: Checks in class declarations that the declared class name+--   is not equal to the name of a primitive type.++prop_checkLocalClassNotPrim d =+  checkInClass d $ \d' ->+    isNotPrimitive (className d')++++-- | Property: Checks in class declarations that no FixedTypeExpression +--   occurs.++prop_checkLocalClassNoFixedTEs d =+  checkInClass d $ \d' ->+    not (hasFixedTypeExpressions d')++++-- | Property: Checks in type signatures that no FixedTypeExpression occurs.++prop_checkLocalSignatureNoFixedTEs d =+  checkInSignature d $ \d' ->+    not (hasFixedTypeExpressions d')++++-- | Property: Checks in data declarations that there is no type abstraction+--   and no function type constructor.++prop_checkLocalDataAbsFun d = prop_checkAbsFun [DataDecl d] forcedCheck+  where types = d :: DataDeclaration++++-- | Property: Checks in newtype declarations that there is no type abstraction+--   and no function type constructor.++prop_checkLocalNewtypeAbsFun d = prop_checkAbsFun [NewtypeDecl d] forcedCheck+  where types = d :: NewtypeDeclaration++++-- | Helper function to check that a value does not contain type abstractions+--   nor function type constructors.++prop_checkAbsFun d test = test hasNoAbsNorFun . runCheck $ d+  where+    runCheck = fst . runWriter . checkDataAndNewtypeDeclarations+    +    hasNoAbsNorFun = everything (&&) (True `mkQ` noAbsFun)+    +    noAbsFun t = case t of+      TypeFun _ _   -> False+      TypeAbs _ _ _ -> False+      otherwise     -> True++++++-- Test helper functions ------------------------------------------------------+++-- | Runs a local check on a data declaration.++checkInData :: DataDeclaration -> (DataDeclaration -> Bool) -> Property+checkInData d prop = +  trivialCheck prop . mapMaybe toData . runLocalCheck $ [DataDecl d]+  where+    toData d = case d of { DataDecl d' -> Just d' ; otherwise -> Nothing }++++-- | Runs a local check on a newtype declaration.++checkInNewtype :: NewtypeDeclaration -> (NewtypeDeclaration -> Bool) -> Property+checkInNewtype d prop =+  forcedCheck prop . mapMaybe toNewtype . runLocalCheck $ [NewtypeDecl d]+  where+    toNewtype d = case d of { NewtypeDecl d' -> Just d' ; otherwise -> Nothing }++++-- | Runs a local check on a type declaration.++checkInType :: TypeDeclaration -> (TypeDeclaration -> Bool) -> Property+checkInType d prop = +  forcedCheck prop . mapMaybe toType . runLocalCheck $ [TypeDecl d]+  where+    toType d = case d of { TypeDecl d' -> Just d' ; otherwise -> Nothing }++++-- | Runs a local check on a class declaration.++checkInClass :: ClassDeclaration -> (ClassDeclaration -> Bool) -> Property+checkInClass d prop = +  forcedCheck prop . mapMaybe toClass . runLocalCheck $ [ClassDecl d]+  where+    toClass d = case d of { ClassDecl d' -> Just d' ; otherwise -> Nothing }++++-- | Runs a local check on a type signature.++checkInSignature :: Signature -> (Signature -> Bool) -> Property+checkInSignature d prop = +  forcedCheck prop . mapMaybe toSig . runLocalCheck $ [TypeSig d]+  where+    toSig d = case d of { TypeSig d' -> Just d' ; otherwise -> Nothing }++++-- | Runs a check on the head of a list. This check forces the list ot have at+--   least one element.++forcedCheck :: (a -> Bool) -> [a] -> Property+forcedCheck prop xs = not (null xs) ==> prop (head xs)++++-- | Runs a trivial check on a list. If the list is empty, the property is not+--   checked.++trivialCheck :: (a -> Bool) -> [a] -> Property+trivialCheck prop xs = +  trivial (null xs) (if null xs then True else prop (head xs))++++-- | Runs a local check.++runLocalCheck :: [Declaration] -> [Declaration]+runLocalCheck = fst . runWriter . checkLocal++++-- | Tests if an identifier is not equal to one of the primitive type names.++isNotPrimitive :: Identifier -> Bool+isNotPrimitive i =+  unpackIdent i `notElem` [ "Int", "Integer", "Float", "Double", "Char" ]++++-- | Tests if a given element contains FixedTypeExpressions.++hasFixedTypeExpressions :: (Typeable a, Data a) => a -> Bool+hasFixedTypeExpressions =+  everything (||) (False `mkQ` (const True :: FixedTypeExpression -> Bool))++++-- | Tests if an element is nested.++isNested :: (Typeable a, Data a) => Identifier -> a -> Bool+isNested con = everything (||) (False `mkQ` nested)+  where+    nested t = case t of+      TypeCon (Con c) ts -> (c == con) && (any (not . isTypeVar) ts)+      otherwise          -> False++    isTypeVar t = case t of+      TypeVar _ -> True+      otherwise -> False++++-- | Tests if an element is recursive.++isRecursive :: (Typeable a, Data a) => Identifier -> a -> Bool+isRecursive con = everything (||) (False `mkQ` (\c -> c == con))+++

@@ -0,0 +1,77 @@+++module FrontendOtherTests (tests) where++++import Control.Monad (liftM)+import Control.Monad.Writer (runWriter)+import Data.Generics (gcount, mkQ)+import Data.Maybe (mapMaybe)+import Data.Set as Set (isSubsetOf)+import Test.QuickCheck ++import Tests++import Language.Haskell.FreeTheorems.Syntax+import Language.Haskell.FreeTheorems.ValidSyntax+import Language.Haskell.FreeTheorems.Frontend as FT+import Language.Haskell.FreeTheorems.Frontend.TypeExpressions+import Language.Haskell.FreeTheorems.Frontend.CheckLocal+import Language.Haskell.FreeTheorems.Frontend.CheckGlobal++++-- | Runs all tests.++tests :: IO ()+tests = do+  doTest "replaceTypeSynonyms is complete" prop_replaceTypeSynonymsIsComplete+  doTest "check is stable" prop_checkIsStable+++++++-- | Property: Replacing every type synonym in a type expression does not leave+--   any type synonym.++prop_replaceTypeSynonymsIsComplete ds = +  withTypeDecls ds $ \ts ->+    let ds' = getDeclarations ds+    in countTypeConSyn ts (replaceAllTypeSynonyms ts ds') == 0++countTypeConSyn ts = gcount (False `mkQ` select)+  where +    select con = case con of+      Con c     -> c `elem` map typeName ts+      otherwise -> False++++-- | Checks a list of declarations and filters all type declarations which then+--   are fed to a property.++withTypeDecls :: ListOfDeclarations -> ([TypeDeclaration] -> Bool) -> Property+withTypeDecls ds prop =+  let getTypeSyn d = case d of { TypeDecl d -> Just d ; otherwise -> Nothing }+      process ds = fst . runWriter $ checkLocal ds >>= checkGlobal []+      typeSyns = mapMaybe getTypeSyn . process . getDeclarations $ ds+   in trivial (null typeSyns) $ prop typeSyns+++++-- | Property: Checks that applying 'check' twice does not more that applying+--   'check once.++prop_checkIsStable ds = +  let once  ds = FT.check ds+      twice ds = FT.check . map rawDeclaration =<< FT.check ds+      count f = length . fst . runWriter . f . getDeclarations $ ds+   in count once == count twice ++++

@@ -0,0 +1,314 @@++++module FrontendTypeExpressionsTests (tests) where++++import Data.Generics (everything, something, somewhere, mkQ, gcount, mkM)+import Data.Map as Map (elems, keysSet, singleton, insert, fromList)+import Data.Set as Set+    ( isSubsetOf, union, member, null, intersection, fromList, difference+    , empty, size, singleton )++import Tests+import Language.Haskell.FreeTheorems.Syntax+import Language.Haskell.FreeTheorems.Frontend.TypeExpressions++++-- | Runs all tests.++tests :: IO ()+tests = do+  doTest "freeVariables are in allVariables" prop_freeVariablesAllVariables+  doTest "every variable is free or bound" prop_freeVariablesBoundVariables+  doTest "allVariables finds at least one variable of a type "+    prop_variablesAreFound+  doTest "closure binds free variables" prop_closureVariables+  doTest "freeVariables . closure == []" prop_closureFreeVariables+  doTest "closureFor emptySet == id" prop_closureForEmptySet+  doTest "count after closure is correct" prop_closureCount+  doTest "createNewTypeVariable creates unique variables"+    prop_createNewTypeVariableNotIn+  doTest"count after alphaConversion is correct" prop_alphaConversionCount+  doTest "alphaConversion keeps freeVariables" prop_alphaConversionFreeVariables+  doTest "alphaConversion substitutes a variable" prop_alphaConversionVariable+  doTest "substituteVariable replaces free variable"+    prop_substituteTypeVariableReplacesFreeVariables+  doTest "substituteVariable keeps free variables"+    prop_substituteTypeVariableKeepsFreeVariables+  doTest "type is contained after substituteTypeVariables"+    prop_substituteTypeVariableTypeInserted+  doTest "count after substituteVariable is correct"+    prop_substituteTypeVariableWithCount++++++------- Test properties -------------------------------------------------------+++-- | Property: Free variables of a type expression are a subset of all+--   type variables occurring in a type expression.++prop_freeVariablesAllVariables t = +  freeTypeVariables t `Set.isSubsetOf` allTypeVariables t+  where types = t :: TypeExpression++++-- | Property: Every type variable occurring in a type expression is free or+--   bound.++prop_freeVariablesBoundVariables t = (free `Set.union` bound) == all+  where +    types = t :: TypeExpression+    free  = freeTypeVariables t+    all   = allTypeVariables  t+    bound = boundVariables t++++-- | Property: If a type expression contains at least one variable, it is also+--   found by allTypeVariables.++prop_variablesAreFound t =+  maybe True (\v -> v `Set.member` allTypeVariables t) (getVariableFrom t)+  where +    types = t :: TypeExpression++++-- | Property: Given a set of type variables, the closure of a type expression+--   for this set does not contain free type variables in that set.++prop_closureVariables t vs =+  Set.null (set `Set.intersection` freeTypeVariables (closureFor set t))+  where+    types = (t :: TypeExpression, vs :: [TypeVariable])+    set = Set.fromList vs++++-- | Property: There are no free type variables after closing a type expression+--   for all free type variables.++prop_closureFreeVariables t =+  Set.null . freeTypeVariables . closureFor (freeTypeVariables t) $ t+  where+    types = t :: TypeExpression++++-- | Property: The closure for an empty set of type variables does not change a+--   type expression.++prop_closureForEmptySet t = closureFor Set.empty t == t+  where+    types = t :: TypeExpression+  +++-- | Property: The count of type constructors does not increase by the closure.++prop_closureCount t vs = +  countTypeAbs t + Set.size set == countTypeAbs (closureFor set t)+  && countTypeFun t == countTypeFun (closureFor set t)+  && countTypeCon t == countTypeCon (closureFor set t)+  where+    types = (t :: TypeExpression, vs :: [TypeVariable])+    set = Set.fromList vs++++-- | Property: A newly created type variable does not occur in the list of+--   forbidden type variables.++prop_createNewTypeVariableNotIn vs =+  not (createNewTypeVariableNotIn s `Set.member` s)+  where+    types = vs :: [TypeVariable]+    s = Set.fromList vs++++-- | Property: Alpha conversion does not increase or decrease the number of+--   type constructors.++prop_alphaConversionCount t v =+  countTypeCon t == countTypeCon (alphaConversion v t)+  && countTypeAbs t == countTypeAbs (alphaConversion v t)+  && countTypeFun t == countTypeFun (alphaConversion v t)+  where types = (t :: TypeExpression, v :: TypeVariable)++++-- | Property: Alpha conversion keeps free variables free.++prop_alphaConversionFreeVariables t v =+  freeTypeVariables t == freeTypeVariables (alphaConversion v t)+  where types = (t :: TypeExpression, v :: TypeVariable)++++-- | Property: After alpha conversion, the replaced variable does not occur+--   in the type expression (except as free variable) and is not bound anymore.++prop_alphaConversionVariable t v =+  (v `Set.member` freeAfterAC || not (v `Set.member` allAfterAC))+  && not (v `Set.member` boundVariables acT)+  where+    types = (t :: TypeExpression, v :: TypeVariable)+    acT = alphaConversion v t+    allAfterAC  = allTypeVariables acT+    freeAfterAC = freeTypeVariables acT++++-- | Property: Replacing type variables with (closed) type expressions in a+--   type expression removes the free variables from the latter type+--   expression (as long as they are not free in any type expression which is+--   inserted).++prop_substituteTypeVariableReplacesFreeVariables (v1,v2) (t1,t2) t =+  (not (v1 `Set.member` vs)+   || v1 `Set.member` freeTypeVariables (fooCon (Map.elems m))+   || not (v1 `Set.member` freeTypeVariables rt))+  &&+  (not (v2 `Set.member` vs)+   || v2 `Set.member` freeTypeVariables  (fooCon (Map.elems m))+   || not (v2 `Set.member` freeTypeVariables rt))++  where+    types = (v1 :: TypeVariable, v2 :: TypeVariable,+             t1 :: TypeExpression, t2 :: TypeExpression,+             t :: TypeExpression)+    m  = Map.fromList [(v1,t1), (v2,t2)]+    vs = Map.keysSet m+    rt = substituteTypeVariables m t+    fooCon = TypeCon (Con $ Ident "Foo")+    +++-- | Property: Replacing a type variable in a type expression keeps the other+--   free variables free.++prop_substituteTypeVariableKeepsFreeVariables (v1,v2) (t1,t2) t i =+  (freeT `Set.difference` vs) `Set.isSubsetOf` freeR+  where+    types = (v1 :: TypeVariable, v2 :: TypeVariable,+             t1 :: TypeExpression, t2 :: TypeExpression, +             t :: TypeExpression, i :: Int)+    m1 = Map.singleton v1 t1+    m  = if i `mod` 2 == 0 then m1 else Map.insert v2 t2 m1+    vs = Map.keysSet m+    rt = substituteTypeVariables m t+    freeT = freeTypeVariables t+    freeR = freeTypeVariables rt++++-- | Property: If a type variable which should be substituted by a type+--   expression is free, then the type expression must occur in the result.++prop_substituteTypeVariableTypeInserted (v1,v2) (t1,t2) t =+  (not (v1 `Set.member` freeTypeVariables t) || t1 `occursIn` rt)+  &&+  (not (v2 `Set.member` freeTypeVariables t) || t2 `occursIn` rt)+  where+    types = (v1 :: TypeVariable, v2 :: TypeVariable,+             t1 :: TypeExpression, t2 :: TypeExpression,+             t :: TypeExpression)+    m  = Map.fromList [(v1,t1), (v2,t2)]+    vs = Map.keysSet m+    rt = substituteTypeVariables m t++++-- | Property: Replacing a type variable increases only the number of type+--   constructors.++prop_substituteTypeVariableWithCount (v1,v2) (t1,t2) t i =+  countTypeFun rt >= countTypeFun t+  && countTypeAbs rt >= countTypeAbs t+  && countTypeCon rt >= countTypeCon t+  where+    types = (v1 :: TypeVariable, v2 :: TypeVariable,+             t1 :: TypeExpression, t2 :: TypeExpression, +             t :: TypeExpression, i :: Int)+    m1 = Map.singleton v1 t1+    m  = if i `mod` 2 == 0 then m1 else Map.insert v2 t2 m1+    vs = Map.keysSet m+    rt = substituteTypeVariables m t++++++-- Test helper functions ------------------------------------------------------++++-- | Returns a set of all bound variables of a type expression.++boundVariables t = everything Set.union (Set.empty `mkQ` select) t+  where+    select t = case t of+      TypeAbs v _ _ -> Set.singleton v +      otherwise     -> Set.empty++++-- | Returns the first variable found in a type expression.+getVariableFrom t = something (Nothing `mkQ` select) t+  where+    select t = case t of+      TypeVar v     -> Just v+      TypeAbs v _ _ -> Just v+      otherwise     -> Nothing++++-- | Counts the number of user-defined type constructors.++countTypeCon t = gcount (False `mkQ` select) t+  where+    select t = case t of+      TypeCon _ _ -> True+      otherwise   -> False++++-- | Counts the number of function type constructors.++countTypeFun t = gcount (False `mkQ` select) t+  where+    select t = case t of+      TypeFun _ _ -> True+      otherwise   -> False++++-- | Counts the number of type abstraction constructors. ++countTypeAbs t = gcount (False `mkQ` select) t+  where+    select t = case t of+      TypeAbs _ _ _ -> True+      otherwise     -> False++++-- | Returns True if t1 occurs in t2.++t1 `occursIn` t2 = case somewhere (mkM $ findT t2) t1 of+  Nothing -> False+  Just _  -> True+  where+    findT t1 t2 = if (t1 == t2) then Just t1 else Nothing++++

@@ -0,0 +1,100 @@+++++module InterpretationTests (tests) where++++tests :: IO ()+tests = do+  return ()+++++{-+-- Helper functions -----------------------------------------------------------++++-- | Counts the number of relational actions of the function type constructor.++countRelFun t = gcount (False `mkQ` select) t+  where+    select t = case t of+      RelFun _ _ _ -> True+      otherwise    -> False++++-- | Counts the number of relational actions of the type abstraction+--   constructor.++countRelAbs t = gcount (False `mkQ` select) t+  where+    select t = case t of+      RelAbs _ _ _ -> True+      otherwise    -> False++++-- | Counts the number of relational actions of nullary type constructors.++countRelBasic t = gcount (False `mkQ` select) t+  where+    select t = case t of+      RelBasic _   -> True+      otherwise -> False++++-- | Counts the number of relational actions for n-ary type constructors.++countRelLift t = gcount (False `mkQ` select) t+  where+    select t = case t of+      RelLift _ _ -> True+      otherwise   -> False++++-- Define the test properties -------------------------------------------------++++-- | Property: The number of type constructors must equal the number of+--   corresponding relations.++prop_interpretCount t l =+  countTypeFun t' == countRelFun rel+  && countTypeAbs t' == countRelAbs rel+  && countTypeCon t' == countRelLift rel + countRelBasic rel+  where+    types = (t :: TypeExpression, l :: LanguageSubset)+    t' = closure t+    sig = ValidSignature (Signature (Ident "x") t')+    Intermediate _ rel = interpret l sig++++-- Run the tests --------------------------------------------------------------++++-- | The main function which runs the list of tests.++main = do+  t "count after interpretation is ok                   "+    prop_interpretCount++  where+    t desc prop = do+      putStr $ desc ++ " ... "+      -- quickCheck prop+      check (defaultConfig {configMaxTest = 100}) prop++-}+++

@@ -0,0 +1,197 @@++++-- | Data structures and functions to automatically generate free theorems.+--+--   This library is based on the following papers:+--+--   * /Theorems For Free!/, Philip Wadler, in Functional Programming Languages+--     and Computer Architecture Proceedings, 1989.+--     <http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps>+--+--   * /The Impact of seq on Free Theorems-Based Program Transformations/,+--     Patricia Johann and Janis Voigtl&#xE4;nder, Fundamenta Informaticae,+--     2006. <http://www.orchid.inf.tu-dresden.de/~voigt/seqFinal.pdf>+--+--+--   The intended usage of this library is as follows.+--   +--   (1) Parse a list of declarations using one of two parsers +--       ('Language.Haskell.FreeTheorems.Parser.Haskell98.parse' or +--       'Language.Haskell.FreeTheorems.Parser.Hsx.parse') or any other+--       suitable parser.+--       Use 'check' to obtain a list of valid declarations.+--+--   (2) Optional:+--       Parse more declarations and validate them against the previously +--       loaded list of valid declarations with 'checkAgainst'.+--+--   (3) Extract all valid signatures from a list of valid declarations by+--       'filterSignatures'.+--+--   (4) Interpret a signature ('interpret'), transform it to a theorem+--       ('asTheorem') and pretty-print it ('prettyTheorem').+--+--   (5) Optional: Specialise relation variables to functions +--       ('relationVariables' and 'specialise').+--+--   (6) Optional: Extract lifted relations to show their definition+--       ('unfoldLifts') and pretty-print them ('prettyUnfoldedLift').+--+--   (7) Optional: Extract class constraints to show their definition+--       ('unfoldClasses') and pretty-print them ('prettyUnfoldedClass').+--++module Language.Haskell.FreeTheorems (++    -- * Valid declarations++    -- $restrictions++    ValidDeclaration+  , ValidSignature+  , rawDeclaration+  , rawSignature+  , filterSignatures++    +    -- * Manufacturing valid declarations +    +  , Parsed+  , Checked+  , runChecks+  , check+  , checkAgainst++    +    -- * Generating free theorems++  , LanguageSubset (..)+  , TheoremType (..)+  , Intermediate+  , interpret+  , asTheorem+  , relationVariables+  , specialise+  , specialiseInverse+  , unfoldLifts+  , unfoldClasses+++    -- * Pretty printing+    +    -- | The pretty printer is based on the module \"Text.PrettyPrint\" which+    --   is usually implemented by \"Text.PrettyPrint.HughesPJ\". See there for+    --   information on how to modify documents.++  , PrettyTheoremOption (..)+  , prettyDeclaration+  , prettySignature+  , prettyTheorem+  , prettyRelationVariable+  , prettyUnfoldedLift+  , prettyUnfoldedClass++) where++++import Text.PrettyPrint (Doc, empty)++import Language.Haskell.FreeTheorems.BasicSyntax+import Language.Haskell.FreeTheorems.ValidSyntax+import Language.Haskell.FreeTheorems.Frontend+import Language.Haskell.FreeTheorems.LanguageSubsets+import Language.Haskell.FreeTheorems.Intermediate+import Language.Haskell.FreeTheorems.Theorems+import Language.Haskell.FreeTheorems.Unfold+import Language.Haskell.FreeTheorems.PrettyTypes+import Language.Haskell.FreeTheorems.PrettyTheorems+++++++-- $restrictions+--+--   The restrictions on valid declarations and valid type signatures, above+--   what is already ensured by the stucture of declarations (see +--   "Language.Haskell.FreeTheorems.Syntax"), are as follows:+--+--   For @data@ and @newtype@ declarations:+--+--   * The declared type constructor is not a primitive type, i.e. it is not+--     equal to @Int@, @Integer@, @Float@, @Double@ nor @Char@.+--+--   * The variables occurring on the right-hand side have to be mentioned on+--     the left-hand side, and the left-hand side variables are pairwise+--     distinct.+--   +--   * There is at least one data constructor in the declaration of an+--     algebraic data type.+--+--   * The declaration is not nested, i.e. if the declared type constructor+--     occurs on the right-hand side, it has only type variables as arguments.+--+--   * No 'Language.Haskell.FreeTheorems.Syntax.FixedTypeExpression' occurs+--     in any type expression on the right-hand side.+--+--   * After replacing all type synonyms: No function type constructor and no+--     type abstraction occurs on the right-hand side.+--+--   For @type@ declarations:+--+--   * The declared type constructor is not a primitive type, i.e. it is not+--     equal to @Int@, @Integer@, @Float@, @Double@ nor @Char@.+--+--   * The variables occurring on the right-hand side have to be mentioned on+--     the left-hand side, and the left-hand side variables are pairwise+--     distinct.+--+--   * The declaration is not recursive, i.e. if the declared type constructor+--     occurs nowhere on the right-hand side.+--+--   * There is no group of @type@ declarations which are mutually recursive.+--+--   * No 'Language.Haskell.FreeTheorems.Syntax.FixedTypeExpression' occurs+--     in the type expression on the right-hand side.+--   +--   For @class@ declarations:+--+--   * The declared type class does not equal a primitive type.+--   +--   * The names of the class methods are pairwise distinct. +--   +--   * The class variable occurs in the type expression of every class method.+--   +--   * The name of the class does not occur in a type expression of any class+--     method.+--   +--   * No 'Language.Haskell.FreeTheorems.Syntax.FixedTypeExpression' occurs+--     in a type expression of any class method.+--+--   * The type class hierarchy is acyclic.+--+--   For type signatures:+--   +--   * No 'Language.Haskell.FreeTheorems.Syntax.FixedTypeExpression' occurs+--     in the type expression of a signature.+--+--   Additionally, the following global restrictions need to hold:+--   +--   * There may be at most one declaration only for every name.+--+--   * Every type class occurring in any type expression is declared.+--+--   * Every type constructor occurring in any type expression is declared.+--     Furthermore, the number of arguments to every type constructor has to+--     match the number of type variables the given on the left-hand side of the+--     declaration of that type constructor.+--+--   Type synonyms do not occur in type expressions of valid declarations.+--   Every type expression of a valid declaration is closed. A special case are+--   class methods. Their types have the class variable as the only free type+--   variable.++

@@ -0,0 +1,256 @@++++-- | Declares the basic syntax of a Haskell98 subset enriched with +--   higher-ranked functions. Additionally, it defines small convenience+--   functions. ++module Language.Haskell.FreeTheorems.BasicSyntax where++++import Data.Generics (Typeable, Data)++++-- | A Haskell declaration which corresponds to a @type@, @data@, @newtype@,+--   @class@ or type signature declaration.+--+--   In type expressions, type variables must not be applied to type+--   expressions. Thus, for example, the functions of the @Monad@ class are not+--   expressible.+--   However, in extension to Haskell98, higher-rank types can be expressed.+--   +--   This data type does not reflect all information of a declaration. Only the+--   aspects needed by the FreeTheorems library are covered.++data Declaration+  = TypeDecl TypeDeclaration            -- ^ A @type@ declaration.+  | DataDecl DataDeclaration            -- ^ A @data@ declaration.+  | NewtypeDecl NewtypeDeclaration      -- ^ A @newtype@ declaration.+  | ClassDecl ClassDeclaration          -- ^ A @class@ declaration.+  | TypeSig Signature                   -- ^ A type signature.+  deriving (Eq, Typeable, Data)++++-- | Gets the name of the item declared by a declaration.+--   This is the type constructor for @data@, @newtype@ and @type@ declarations,+--   the name of a class for a @class@ declaration or the name of a type+--   signature.++getDeclarationName :: Declaration -> Identifier+getDeclarationName (DataDecl d)    = dataName d+getDeclarationName (NewtypeDecl d) = newtypeName d+getDeclarationName (TypeDecl d)    = typeName d+getDeclarationName (ClassDecl d)   = className d+getDeclarationName (TypeSig s)     = signatureName s++++-- | Gets the arity of a type constructor or @Nothing@ if this is not a+--   @data@, @newtype@ or @type@ declaration.++getDeclarationArity :: Declaration -> Maybe Int+getDeclarationArity (DataDecl d)    = Just . length . dataVars $ d+getDeclarationArity (NewtypeDecl d) = Just . length . newtypeVars $ d+getDeclarationArity (TypeDecl d)    = Just . length . typeVars $ d+getDeclarationArity (ClassDecl d)   = Nothing+getDeclarationArity (TypeSig s)     = Nothing++++-- | A @type@ declaration for a type synonym.++data TypeDeclaration = Type +  { typeName :: Identifier     -- ^ The type constructor name.+  , typeVars :: [TypeVariable] -- ^ The type variables on the left-hand side.+  , typeRhs  :: TypeExpression -- ^ The type expression on the right-hand side.+  }+  deriving (Eq, Typeable, Data)++++-- | A @data@ declaration for an algebraic data type.+--+--   Note that the context and the deriving parts of a @data@ declaration are+--   ignored.++data DataDeclaration = Data +  { dataName     :: Identifier+        -- ^ The name of the type constructor.++  , dataVars     :: [TypeVariable]+        -- ^ The type variables on the left-hand side.++  , dataCons     :: [DataConstructorDeclaration]+        -- ^ The declarations of the data constructors on the right-hand side.++  }+  deriving (Eq, Typeable, Data)++++-- | A @newtype@ declaration for a type renaming.+--+--   Note that the context and the deriving parts of a @newtype@ declaration are+--   ignored.++data NewtypeDeclaration = Newtype +  { newtypeName     :: Identifier       +        -- ^ The name of the type constructor.+  +  , newtypeVars     :: [TypeVariable]   +        -- ^ The type variables of the left-hand side.+  +  , newtypeCon      :: Identifier+        -- ^ The name of the data constructor on the right-hand side.+  +  , newtypeRhs      :: TypeExpression+        -- ^ The type expression on the right-hand side.+  +  }+  deriving (Eq, Typeable, Data)++++-- | A @class@ declaration for a type class.+--+--   Note that, except of type signatures of class methods, all other+--   declarations inside the class are ignored.++data ClassDeclaration = Class +  { superClasses :: [TypeClass]     +        -- ^ The superclasses of this class.+  +  , className    :: Identifier      +        -- ^ The name of this type class.+  +  , classVar     :: TypeVariable    +        -- ^ The type variable constrained by this type class.+  +  , classFuns    :: [Signature]+        -- ^ The type signatures of the class methods.+  +  }+  deriving (Eq, Typeable, Data)++++-- | A type signature.++data Signature = Signature+  { signatureName :: Identifier     +        -- ^ The name of the signature, i.e. the name of a variable or function.+  +  , signatureType :: TypeExpression+        -- ^ The type expression of the type signature.+  +  }+  deriving (Eq, Typeable, Data)++++-- | An identifier.+--   This data type tags every @String@ occurring in a declaration or a type+--   expression.++newtype Identifier = Ident { unpackIdent :: String }+  deriving (Eq, Ord, Typeable, Data)++++-- | A data constructor declaration.++data DataConstructorDeclaration = DataCon +  { dataConName  :: Identifier+        -- ^ The name of the data constructor.+  +  , dataConTypes :: [BangTypeExpression]+        -- ^ The type arguments of the data constructor.+  +  }+  deriving (Eq, Typeable, Data)++++-- | Indicates whether in an algebraic data type declaration a strictness+--   annotation is used.++data BangTypeExpression+  = Banged { withoutBang :: TypeExpression }+      -- ^ A type expression with a strictness flag \"@!@\".++  | Unbanged { withoutBang :: TypeExpression }+      -- ^ A type expression without a strictness flag.++  deriving (Eq, Typeable, Data)++++-- | A Haskell type expression. This data type supports also higher-rank+--   functions. Unlike in Haskell98, a type variable must not be applied to+--   type expressions.++data TypeExpression+  = TypeVar TypeVariable+      -- ^ A type variable.++  | TypeCon TypeConstructor [TypeExpression]+      -- ^ A type constructor. This covers algebraic data types, type synonyms,+      --   and type renamings as well as predefined standard data types like+      --   lists and tuples.++  | TypeFun TypeExpression TypeExpression+      -- ^ The function type constructor @->@.++  | TypeAbs TypeVariable [TypeClass] TypeExpression+      -- ^ The type abstraction constructor @forall@.++  | TypeExp FixedTypeExpression+      -- ^ A variable representing a fixed type expression.++  deriving (Eq, Typeable, Data)++++-- | The data type for type constructors.++data TypeConstructor+  = ConUnit        -- ^ The unit type constructor @()@.+  | ConList        -- ^ The list type constructor @[]@.+  | ConTuple Int   -- ^ The tuple type constructors with given arity.+  | ConInt         -- ^ The Haskell type @Int@.+  | ConInteger     -- ^ The Haskell type @Integer@.+  | ConFloat       -- ^ The Haskell type @Float@.+  | ConDouble      -- ^ The Haskell type @Double@.+  | ConChar        -- ^ The Haskell type @Char@.+  | Con Identifier -- ^ Any other type constructor with a given name.+  deriving (Eq, Typeable, Data)++++-- | Identifies a Haskell type class.++newtype TypeClass = TC Identifier+  deriving (Eq, Typeable, Data)++++-- | Identifies a Haskell type variable++newtype TypeVariable = TV Identifier+  deriving (Eq, Ord, Typeable, Data)++++-- | Represents an abbreviation for some fixed type expression.+--   It does not occur in Haskell98 source code, but it can occur in generated+--   theorems.++newtype FixedTypeExpression = TF Identifier+  deriving (Eq, Typeable, Data)++++

@@ -0,0 +1,136 @@++++-- | Defines functions to ensure that only valid declarations and type +--   signatures are fed to the FreeTheorems library. The given functions are+--   intended as second stage after parsing declarations.++module Language.Haskell.FreeTheorems.Frontend (+    Checked+  , Parsed+  , runChecks+  , check+  , checkAgainst+) where++++import Data.Generics (everything, extQ, mkQ)+import Data.List (partition, intersect)+import Data.Maybe (mapMaybe)++import Language.Haskell.FreeTheorems.Syntax+import Language.Haskell.FreeTheorems.ValidSyntax (ValidDeclaration (..))+import Language.Haskell.FreeTheorems.Frontend.Error (Checked, Parsed, runChecks)+import Language.Haskell.FreeTheorems.Frontend.TypeExpressions+    (replaceAllTypeSynonyms, closeTypeExpressions)+import Language.Haskell.FreeTheorems.Frontend.CheckLocal+    (checkLocal, checkDataAndNewtypeDeclarations)+import Language.Haskell.FreeTheorems.Frontend.CheckGlobal (checkGlobal)++++-- | Checks a list of declarations.+--   It returns a list of all declarations which are valid and an error message+--   for all those declarations which are not valid.++check :: [Declaration] -> Checked [ValidDeclaration]+check = checkAgainst []++++-- | Checks a list of declarations against a given list of valid+--   declarations.+--   It returns a list of all declarations from the second argument which are+--   valid. Moreover, the result contains an error message for all those+--   declarations which are not valid.+--+--   The declarations given in the second argument may be based on those of the+--   first argument. For example, if the first argument contains a valid+--   declaration of a type \"Foo\" and if the second argument contains the+--   following declaration+--+--   > type Bar = Foo+--+--   then also the declaration of \"Bar\" is valid.++checkAgainst :: +    [ValidDeclaration] +    -> [Declaration] +    -> Checked [ValidDeclaration]++checkAgainst vds ds = +    +    -- start from 'ds'+  return ds+   +    -- perform local checks:+    --   * free variables of the right-hand side are declared on the left-hand+    --     of declarations+    --   * type variables of the left-hand side are pairwise distinct+    --   * primitive types are not declared+    --   * FixedTypeExpression does not occur anywhere+    --   * type synonyms are not recursive+    --   * data and newtype are not nested+    --   * classes methods are pairwise distinct, don't use the owning class+    --     and have the class variable as free variable+  >>= checkLocal+  +    -- perform global checks:+    --   * at most one declaration per name+    --   * arity checks of type constructors in all type expressions+    --   * type class hierarchy is acyclic+    --   * type synonym declarations are not mutually recursive+    --   * all used constructors and classes are declared+  >>= checkGlobal vds++    -- replace all type synonyms, use also the valid type synonyms+  >>= \ds' -> +    let getTypeSyn d = case d of { TypeDecl t -> Just t ; otherwise -> Nothing }+        typeSyns = mapMaybe getTypeSyn (map rawDeclaration vds ++ ds')+     in return (replaceAllTypeSynonyms typeSyns ds')++    -- checks in data and newtype declarations: no abstractions, no functions+  >>= checkDataAndNewtypeDeclarations++    -- finally, close all type signatures and class methods and transform all+    -- declarations to valid ones+  >>= return . makeValid vds . closeTypeExpressions++++-- | Turns a list of declarations into valid declarations.+--   Additionally, every declaration is checked whether it depends on any +--   algebraic data type with strictness flags.++makeValid :: [ValidDeclaration] -> [Declaration] -> [ValidDeclaration]+makeValid vds ds = +  let strict = map rawDeclaration (filter isStrictDeclaration vds)+      knownStrict = map getDeclarationName +                        (strict ++ filter hasStrictnessFlags ds)+      +      rec ss ds = +        let (ns, os) = partition (dependsOnStrictTypes ss) ds+         in if null ns+              then ss+              else rec (ss ++ map getDeclarationName ns) os++      allStrict = rec knownStrict ds+   +   in map (\d -> ValidDeclaration d (getDeclarationName d `elem` allStrict)) ds+  where+    hasStrictnessFlags d = +      let hasBang (Banged _)   = True+          hasBang (Unbanged _) = False+       in everything (||) (False `mkQ` hasBang) d+    +    dependsOnStrictTypes ss d = +      let getCons c = case c of { Con n -> [n] ; otherwise -> [] }+          getClasses (TC n) = [n]+          ns = everything (++) ([] `mkQ` getCons `extQ` getClasses) d+       in not (null (ns `intersect` ss))++ +++

@@ -0,0 +1,418 @@++++-- | Defines global checks, i.e. checks which need to look at more than one+--   declaration at a time.++module Language.Haskell.FreeTheorems.Frontend.CheckGlobal (checkGlobal) where++++import Control.Monad (when)+import Control.Monad.Error (throwError)+import Control.Monad.Writer (tell)+import Data.Generics (Typeable, Data, everything, everywhereM, extQ, mkQ, mkM)+import Data.List (intersperse, partition, nub, intersect)+import qualified Data.Map as Map (Map, empty, insert, lookup)+import Data.Maybe (mapMaybe, fromJust)+import qualified Data.Set as Set+    ( Set, empty, singleton, union, fromList, isSubsetOf, member, difference+    , partition, null, elems, size )++import Language.Haskell.FreeTheorems.BasicSyntax+import Language.Haskell.FreeTheorems.ValidSyntax+import Language.Haskell.FreeTheorems.Frontend.Error++++++------- Global checks ---------------------------------------------------------+++-- | Perform global checks, i.e. looks at more than one declaration at a time.+--   The following restrictions will be checked:+--+--   * Every symbol is declared at most once.+--   +--   * Every type constructor is used in the arity it was declared with.+--+--   * Type synonyms are not mutually recursive.+--+--   * The type class hierachy is acyclic.+--+--   * In every type expression, only declared type constructors and only+--     declared type classes occur.++checkGlobal :: [ValidDeclaration] -> [Declaration] -> Checked [Declaration] +checkGlobal vds ds =+  -- run through all declarations in 'ds' to test whether any name occurs twice+  checkUnique vds ds++  -- then, run through all remaining declarations and check the arities of all+  -- type constructors+  >>= checkArities vds++  -- extract all type synonyms which are not mutually recursive+  >>= checkAcyclicTypeSynonyms++  -- extract all type classes whose type hierarchy is acyclic+  >>= checkAcyclicTypeClasses++  -- finally, take only those declarations which contain only declared type+  -- constructors and type classes+  >>= checkAllConsAndClassesDeclared vds++++++------- Check that declarations are unique ------------------------------------+++-- | Checks that every name has at most one declaration, or that there are no+--   two declarations with the same name.+--+--   The first argument gives a list of already checked declarations against+--   which the second argument is tested. The resulting list contains all+--   elements of the first argument and only the valid declarations of the+--   second argument.++checkUnique :: [ValidDeclaration] -> [Declaration] -> Checked [Declaration]+checkUnique vds ds =+  let -- extract all known declaration names, both from 'vds' and from 'ds'+      knownNames = map getDeclarationName (map rawDeclaration vds ++ ds)+    +      -- test if the name of a declaration occurs more than once in 'knownNames'+      occursMoreThanOnce d = +        let allOccurrences = filter (== (getDeclarationName d)) knownNames+         in length allOccurrences > 1+ +      -- construct a list 'us' of all unique declarations and a list 'ms' of all+      -- declarations which names occur more than once+      (ms, us) = partition occursMoreThanOnce ds++      -- extract the names which occur more than once+      multiples = map unpackIdent . nub . map getDeclarationName $ ms++      error s = [pp ("Multiple declarations for `" ++ s ++ "'.")]+   +   in do when (not (null multiples)) $ mapM_ (tell . error) multiples+         return us++++++------- Check arities of type constructors ------------------------------------+++-- | Checks the arity of all type constructors. If an undeclared type+--   constructor is found, no arity check will be performed, because+--   any declaration containing undeclared type constructors will be filtered+--   out in the next step of checking (see 'checkGlobal').++checkArities :: [ValidDeclaration] -> [Declaration] -> Checked [Declaration]+checkArities vds ds =+  let -- build a map of arities+      mkMap d m = case getDeclarationArity d of+                    Nothing     -> m+                    Just arity  -> Map.insert (getDeclarationName d) arity m+      arityMap = foldr mkMap Map.empty (map rawDeclaration vds ++ ds)++   in foldChecks (\d -> inDecl d $ checkArity arityMap d) ds++++-- | Checks the arities of all occurring type constructors according to the +--   given arity map.++checkArity :: (Typeable a, Data a) => Map.Map Identifier Int -> a -> ErrorOr a+checkArity arityMap = everywhereM (mkM checkCorrectArity)+  where+    -- extracts the type constructors and relates expected and found arities+    checkCorrectArity t = case t of+      TypeCon ConUnit ts    -> errorArity t "()"      0 (length ts)+      TypeCon ConList ts    -> errorArity t "[]"      1 (length ts)+      TypeCon ConInt ts     -> errorArity t "Int"     0 (length ts)+      TypeCon ConInteger ts -> errorArity t "Integer" 0 (length ts)+      TypeCon ConFloat ts   -> errorArity t "Float"   0 (length ts)+      TypeCon ConDouble ts  -> errorArity t "Double"  0 (length ts)+      TypeCon ConChar ts    -> errorArity t "Char"    0 (length ts)+      TypeCon (Con c) ts    -> case Map.lookup c arityMap of+                                 Nothing -> return t+                                 Just i  -> let n = unpackIdent c+                                             in errorArity t n i (length ts)+      +      TypeCon (ConTuple n) ts -> do+        errorArity t ("(" ++ replicate (n-1) ',' ++ ")") n (length ts)+        errorIf (n < 2) $+          pp "A tuple type constructor must have at least two arguments."+        return t+                                 +      otherwise             -> return t++    -- performs the actual checking and error message creation+    errorArity t conName expected found = +      let args k = case k of+            0         -> "no argument"+            1         -> "1 argument"+            otherwise -> show k ++ " arguments"+       in do errorIf (found /= expected) $+                pp ("Type constructor `" ++ conName ++ "' was declared to have "+                    ++ args expected ++ ", but it is used with " ++ args found +                    ++ ".")+             return t+   +++++------- Acyclic tests ---------------------------------------------------------+++-- | Checks that type synonym declarations are not mutually recursive.+--   Error messages are created for all type synonym declarations which are+--   mutually recursive with other type synonym declarations.++checkAcyclicTypeSynonyms :: [Declaration] -> Checked [Declaration]+checkAcyclicTypeSynonyms ds =+  let -- gets the name of a type synonym declaration or Nothing+      getTypeSynonymName d = +        case d of { TypeDecl d -> Just (typeName d) ; otherwise -> Nothing }+      +      -- the list of all known type synonym names+      allTypeSynonymNames = mapMaybe getTypeSynonymName ds++      -- extracts a type synonym name from a type expression+      occurringTypeSynonyms t = case t of+        TypeCon (Con c) _ -> if c `elem` allTypeSynonymNames +                               then Set.singleton c+                               else Set.empty+        otherwise         -> Set.empty+      +      -- given an element (e.g. a declaration), this function determines all+      -- type synonyms which this element is based on+      getDependencies = +        everything Set.union (Set.empty `mkQ` occurringTypeSynonyms)++      -- the error message for all unaccepted declarations+      error = "Declarations of type synonyms must not be mutually recursive."++      -- filter all mutually recursive declarations+   in checkDependencyGraph ds getDependencies error "type synonym"++++-- | Checks that the type class hierarchy is acyclic. An error message is+--   created for every type class which is part of a cycle.+--+--   Undeclared type classes occurring as superclasses are ignored. They will+--   be filtered out in the next step (see 'checkGlobal').++checkAcyclicTypeClasses :: [Declaration] -> Checked [Declaration]+checkAcyclicTypeClasses ds =+  let -- gets the name of a class declaration or Nothing+      getClassName d = +        case d of { ClassDecl d -> Just (className d) ; otherwise -> Nothing }+      +      -- the list of all known class names+      allClassNames = mapMaybe getClassName ds++      -- given a class declaration, this function returns the set of all+      -- superclasses having a known declaration+      getSuperClasses d = case d of+        ClassDecl d -> let cs = map (\(TC c) -> c) . superClasses $ d+                        in Set.fromList (cs `intersect` allClassNames)+        otherwise   -> Set.empty++      -- the error message for all unaccepted declarations+      error =+        "The type class hierarchy formed by the type classes and their "+        ++ "superclasses must not be acyclic."++      -- filter all acyclic type classes+   in checkDependencyGraph ds getSuperClasses error "type class"++++-- | Applies 'recursivePartition' to the arguments and generates error messages+--   for all erroneous declarations.++checkDependencyGraph :: +    [Declaration] +    -> (Declaration -> Set.Set Identifier) +    -> String+    -> String+    -> Checked [Declaration]++checkDependencyGraph ds getDependencies errMsg tag = do+  let (ok, err) = recursivePartition ds getDependencies+  when (not (null err)) $+    tell [pp (errMsg+              ++ violating tag +                   (map (unpackIdent . getDeclarationName . fst) err))]+  return ok++++-- | Partitions a list of declarations using a dependency function.+--   Every declaration, which depends only on the declarations given by the+--   third argument, is put into the left set.+--   Every declaration, which depends only on the declarations already in the+--   left set, is put also into the left set. This step is recursively repeated+--   until no more declarations are added to the left set.+--   This function terminates if the first argument is a finite list.++recursivePartition :: +    [Declaration] +    -> (Declaration -> Set.Set Identifier) +    -> ([Declaration], [(Declaration, Set.Set Identifier)])++recursivePartition decls getDependencies =+  let -- to increase efficency, calculate the dependencies beforehand+      -- and use the declaration names as keys (declaration names are unique)+      mkMap d m = Map.insert (getDeclarationName d) (getDependencies d) m+      depMap = foldr mkMap Map.empty decls++      -- checks if 'd' depends only on 'ds' and 'extras', +      -- i.e. if 'd' is fully contained in 'ds' and 'extras'+      dependsOn d ds = +        let deps = fromJust (Map.lookup d depMap)+         in deps `Set.isSubsetOf` ds++      -- implements the actual partitioning+      select (ds, rs) = +        let (ds', rs') = Set.partition (\d -> d `dependsOn` ds) rs+         in if Set.null ds'+              then (ds, rs)+              else select (ds `Set.union` ds', rs')++      -- run the partitioning, 'ok' is the accepted set while 'err' contains+      -- all erroneous declarations+      (s1, s2) = select (Set.empty, Set.fromList (map getDeclarationName decls))+      (ok, err) = partition (\d -> getDeclarationName d `Set.member` s1) decls++      -- reduce the mapping to erroneous declarations only such that every+      -- declaration is only mapped to names of erroneous declarations+      getErrDeps d = +        let deps = fromJust (Map.lookup (getDeclarationName d) depMap)+         in deps `Set.difference` s1+      errMap = foldr (\d m -> (d, getErrDeps d) : m) [] err++   in (ok, errMap)++++++------- Check declared type constuctors and classes ---------------------------+++data Name+  = CON Identifier+  | CLA Identifier+  | OTH Identifier+  deriving (Eq, Ord)+++getDeclarationName' :: Declaration -> Name+getDeclarationName' (TypeDecl d)    = CON (typeName d)+getDeclarationName' (DataDecl d)    = CON (dataName d)+getDeclarationName' (NewtypeDecl d) = CON (newtypeName d)+getDeclarationName' (ClassDecl d)   = CLA (className d)+getDeclarationName' (TypeSig s)     = OTH (signatureName s)+++unpackName :: Name -> Identifier+unpackName (CON c) = c+unpackName (CLA c) = c+unpackName (OTH c) = c++++-- | Checks that all declarations depend only on declared type constructors and+--   declared type classes.++checkAllConsAndClassesDeclared :: +    [ValidDeclaration] -> [Declaration] -> Checked [Declaration]+checkAllConsAndClassesDeclared vds ds = +  let -- gets a type constructor name occurring in a type expression+      getCons t = case t of+        TypeCon (Con c) _ -> Set.singleton (CON c)+        otherwise         -> Set.empty++      -- gets a type class name+      getClasses (TC c) = Set.singleton (CLA c)++      -- gets all type class names and all type constructor names occurring+      -- in an element (e.g. a declaration)+      getDependencies = +        everything Set.union (const Set.empty `extQ` getCons `extQ` getClasses)++      -- the error message for all unaccepted declarations+      error d is = +        inDecl d $+          throwError $+            pp ("The following type constructors or type classes are not "+                ++ "declared or their declaration contains errors: "+                ++ (concat . intersperse ", " . map (unpackIdent . unpackName) +                   $ is))++      (ok, err) = partitionDeclared ds getDependencies (map rawDeclaration vds)++      -- filter all declarations which only depend on declared type constructors+      -- and declared type classes+   in do tell (mapMaybe (\(d, is) -> getError . error d . Set.elems $ is) err)+         return ok+  +++-- | Partitions a given list to all those declarations which don't rely +--   directly or indirectly on undeclared type constructors or type classes.+--   Compare with 'recursivePartition'.++partitionDeclared :: +    [Declaration] +    -> (Declaration -> Set.Set Name) +    -> [Declaration]+    -> ([Declaration], [(Declaration, Set.Set Name)])++partitionDeclared decls getDependencies extraDecls =+  let -- to increase efficency, calculate the dependencies beforehand+      -- and use the declaration names as keys (declaration names are unique)+      mkMap d m = Map.insert (getDeclarationName' d) (getDependencies d) m+      depMap = foldr mkMap Map.empty decls++      -- the list of extra names+      extras = Set.fromList (map getDeclarationName' extraDecls)++      -- checks if 'd' depends only on 'ds' and 'extras', +      -- i.e. if 'd' is fully contained in 'ds' and 'extras'+      dependsOn d ds = +        let deps = fromJust (Map.lookup d depMap)+         in deps `Set.isSubsetOf` (extras `Set.union` ds)++      -- implements the actual partitioning+      select (ds, es) = +        let (ds', es') = Set.partition (\d -> d `dependsOn` ds) ds+         in if Set.size ds == Set.size ds'+              then (ds, es)+              else select (ds', es `Set.union` es')++      -- run the partitioning, 'ok' is the accepted set while 'err' contains+      -- all erroneous declarations+      (s1, s2) = select (Set.fromList (map getDeclarationName' decls), Set.empty)+      (ok, err) = partition (\d -> getDeclarationName' d `Set.member` s1) decls++      -- reduce the mapping to erroneous declarations only such that every+      -- declaration is only mapped to names of erroneous declarations+      getErrDeps d = +        let deps = fromJust (Map.lookup (getDeclarationName' d) depMap)+         in deps `Set.difference` (extras `Set.union` s1)+      errMap = foldr (\d m -> (d, getErrDeps d) : m) [] err++   in (ok, errMap)+++

@@ -0,0 +1,397 @@++++-- | Defines local checks, i.e. checks which only look at one declaration at a+--   time.++module Language.Haskell.FreeTheorems.Frontend.CheckLocal (+    checkLocal+  , checkDataAndNewtypeDeclarations+) where++++import Data.Generics (Data, everything, mkQ)+import Data.List (group, sort)+import Data.Maybe (mapMaybe, fromJust, isJust)+import qualified Data.Set as Set+    ( Set, union, empty, difference, fromList, null, elems, isSubsetOf+    , singleton)++import Language.Haskell.FreeTheorems.Syntax+import Language.Haskell.FreeTheorems.Frontend.Error+import Language.Haskell.FreeTheorems.Frontend.TypeExpressions++++++------- Local checks ----------------------------------------------------------+++-- | Check validity of every declaration.+--   This includes ensuring that fixed type expressions occur nowhere, that only+--   declared type variables occur in right-hand sides and that no primitive+--   type is declared, among other restrictions.+--+--   Local checks comprise all those which can be down by just looking at a+--   single declaration.++checkLocal :: [Declaration] -> Checked [Declaration]+checkLocal = foldChecks checkDecl+  where+    checkDecl :: Declaration -> ErrorOr ()+    checkDecl (DataDecl d)    = checkDataDecl d+    checkDecl (NewtypeDecl d) = checkNewtypeDecl d+    checkDecl (TypeDecl d)    = checkTypeDecl d+    checkDecl (ClassDecl d)   = checkClassDecl d+    checkDecl (TypeSig sig)   = checkSignature sig++++-- | Checks a @data@ declaration. The following restrictions must hold:+--   +--   * The declared type constructor is not a primitive type.+--   * The variables occurring on the right-hand side have to be mentioned on+--     the left-hand side, and the left-hand side variables are pairwise+--     distinct.+--   * The declaration is not nested, i.e. if the declared type constructor+--     occurs on the right-hand side, it has only type variables as arguments.+--   * No fixed type expression occurs in any type expression.++checkDataDecl :: DataDeclaration -> ErrorOr ()+checkDataDecl d =+  inDecl (DataDecl d) $ do+    checkNotPrimitive (dataName d)+    checkVariables (dataVars d)+                   (everything Set.union+                      (Set.empty `mkQ` (freeTypeVariables . withoutBang)) +                      (dataCons d))+    checkNotEmpty (dataCons d)+    mapM_ (checkNotNested (dataName d) (map TypeVar (dataVars d)))+          (conNamesAndTypes d)+    mapM_ (checkNoFixedTEsNamed "data constructor") (conNamesAndTypes d)+  where+    conNamesAndTypes = +      map (makePair dataConName (map withoutBang . dataConTypes)) . dataCons++++-- | Checks a @newtype@ declaration. The following restrictions must hold:+--   +--   * The declared type constructor is not a primitive type.+--   * The variables occurring on the right-hand side have to be mentioned on+--     the left-hand side, and the left-hand side variables are pairwise+--     distinct.+--   * The declaration is not nested, i.e. if the declared type constructor+--     occurs on the right-hand side, it has only type variables as arguments.+--   * No fixed type expression occurs in the right-hand side type expression.++checkNewtypeDecl :: NewtypeDeclaration -> ErrorOr ()+checkNewtypeDecl d =+  inDecl (NewtypeDecl d) $ do+    checkNotPrimitive (newtypeName d)+    checkVariables (newtypeVars d) (freeTypeVariables $ newtypeRhs d)+    checkNotNested (newtypeName d) (map TypeVar (newtypeVars d)) (conAndType d)+    checkNoFixedTEsNamed "data constructor" (conAndType d)+  where+    conAndType = makePair newtypeCon (singletonList . newtypeRhs)++++-- | Checks a @type@ declaration. The following restrictions must hold:+--   +--   * The declared type constructor is not a primitive type.+--   * The variables occurring on the right-hand side have to be mentioned on+--     the left-hand side, and the left-hand side variables are pairwise+--     distinct.+--   * The declaration must not be recursive, i.e. the type constructor declared+--     by this declaration must not occur on th right-hand side.+--   * No fixed type expression occurs in the right-hand side type expression.++checkTypeDecl :: TypeDeclaration -> ErrorOr ()+checkTypeDecl d = +  inDecl (TypeDecl d) $ do+    checkNotPrimitive (typeName d)+    checkVariables (typeVars d) (freeTypeVariables $ typeRhs d)+    checkTypeDeclNotRecursive (typeName d) (typeRhs d)+    checkNoFixedTEs (typeRhs d)++++-- | Checks a @class@ declaration. The following restrictions must hold:+--   +--   * The declared type class does not equal a primitive type.+--   * The names of the class methods are pairwise distinct. +--   * The class variable occurs in the type expression of every class method.+--   * The name of the class does not occur in a type expression of any class+--     method.+--   * No fixed type expression occurs in a type expression of any class method.++checkClassDecl :: ClassDeclaration -> ErrorOr ()+checkClassDecl d =+  inDecl (ClassDecl d) $ do+    checkNotPrimitive (className d)+    checkClassMethodsDistinct (map signatureName . classFuns $ d)+    checkClassVarInMethods (classVar d) (classFuns d)+    checkClassDeclNotRecursive (className d) (classFuns d)+    mapM_ (checkNoFixedTEsNamed "class method")+          (map (makePair signatureName (singletonList . signatureType))+               (classFuns d))++++-- | Checks a type signature. The following restrictions must hold:+--   +--   * No fixed type expressions occurs in the type expression of this type+--     signature.++checkSignature :: Signature -> ErrorOr ()+checkSignature s =+  inDecl (TypeSig s) $ do+    checkNoFixedTEs (signatureType s)++++++------- Special checks for data and newtype declarations ----------------------+++-- | Check data and newtype declarations for occurring function type+--   constructors or type abstraction constructors. If any declaration contains+--   one of these, an error message is created. All other declarations are+--   passed.++checkDataAndNewtypeDeclarations :: [Declaration] -> Checked [Declaration]+checkDataAndNewtypeDeclarations = foldChecks checkDN+  where+    checkDN :: Declaration -> ErrorOr ()+    checkDN d = case d of+      DataDecl d'    -> inDecl d (mapM_ checkAbsFun (dataConsAndTypes d'))+      NewtypeDecl d' -> inDecl d (checkAbsFun (newtypeConAndType d'))+      otherwise      -> return ()++    dataConsAndTypes =+      map (makePair dataConName (map withoutBang . dataConTypes)) . dataCons+    +    newtypeConAndType = makePair newtypeCon (singletonList . newtypeRhs)+++++++------- Checking restrictions -------------------------------------------------+++-- | Checks if the given identifier is not a name of a primitive type.+--   Otherwise, an error message is created.++checkNotPrimitive :: Identifier -> ErrorOr ()+checkNotPrimitive (Ident name) =+  errorIf (name `elem` ["Int", "Integer", "Float", "Double", "Char"]) $+    pp ("A primitive type must not have a declaration.")+  +++-- | Checks if the second argument set is contained in the first argument list.+--   If not, an error message is returned.+--+--   Checks also if first argument contains pairwise distinct variables.+--   If not, an error message is returned.++checkVariables :: [TypeVariable] -> Set.Set TypeVariable -> ErrorOr ()+checkVariables vs rvs = do+  let es = extractRepeatingElements vs+  errorIf (not $ null es) $+    pp ("Type variables must not be given more than once on the left-hand "+        ++ "side of a declaration. "+        ++ violating "variable" (map varName $ es))++  let set = rvs `Set.difference` Set.fromList vs+  errorIf (not (Set.null set)) $+    pp ("Type variables occurring on the right-hand side of a declaration must "+        ++ "be declared on the left-hand side. "+        ++ violating "variable" (map varName . Set.elems $ set))++  where+    varName (TV v) = unpackIdent v++++-- | Checks that there is at least one data constructor declaration in the the+--   declaration of an algebraic data type.++checkNotEmpty :: [DataConstructorDeclaration] -> ErrorOr ()+checkNotEmpty cons =+  errorIf (null cons) $+    pp ("The declaration of an algebraic data type must have at least one "+        ++ "data constructor.")++++-- | Checks if the identifiers occurs in any of the given type expressions as+--   a type constructor. If so, and if the identifier is applied not only to+--   type variables, it is called nested and an error message is created.++checkNotNested :: +    Identifier -> [TypeExpression] -> (Identifier, [TypeExpression]) +    -> ErrorOr ()+checkNotNested con vs (dcon, ts) =+  errorIf (any (satisfiesSomewhere isNested) ts) $+    pp ("Declarations must not be nested."+        ++ violating "data constructor" [unpackIdent dcon])+  where+    isNested t = case t of+      TypeCon (Con c) ts -> c == con && ts /= vs+      otherwise          -> False++++-- | Checks if a type declaration is recursive, i.e. the identifier occurs in+--   the given type expression as a type constructor.+--   If so, an error message is created.++checkTypeDeclNotRecursive :: Identifier -> TypeExpression -> ErrorOr ()+checkTypeDeclNotRecursive ident t =+  errorIf (satisfiesSomewhere (isCon ident) t) $+    pp ("A type synonym must not be declared recursively.")+  where+    isCon ident t = case t of+      TypeCon (Con c) _ -> c == ident+      otherwise         -> False++++-- | Checks that the names of class methods are pairwise distinct.+--   If not, an error message is created.++checkClassMethodsDistinct :: [Identifier] -> ErrorOr ()+checkClassMethodsDistinct is =+  let es = extractRepeatingElements is+   in errorIf (not $ null es) $+        pp ("Class methods must not be declared more than once. "+            ++ violating "class method" (map unpackIdent es))++++-- | Checks if the given identifier occurs as free type variable in every+--   signature. If not, an error message is created.++checkClassVarInMethods :: TypeVariable -> [Signature] -> ErrorOr ()+checkClassVarInMethods v@(TV vName) ss =+  let setOfv      = Set.singleton v+      vIsFreeIn t = setOfv `Set.isSubsetOf` freeTypeVariables t+      ms          = filter (not . vIsFreeIn . signatureType) ss+   in errorIf (not $ null ms) $+        pp ("The type variable `" ++ unpackIdent vName ++ "' must occur free "+            ++ "in the type expressions of every class method. "+            ++ violating "class method" (map (unpackIdent . signatureName) ms))+    +++-- | Checks that the name of a type class does not occur in any of the class+--   methods. Otherwise, an error message is created.+checkClassDeclNotRecursive :: Identifier -> [Signature] -> ErrorOr ()+checkClassDeclNotRecursive ident sigs =+  let hasThisClass = satisfiesSomewhere (\c -> c == TC ident)+      ms           = filter (hasThisClass . signatureType) sigs+   in errorIf (not $ null ms) $+        pp ("The type class `" ++ unpackIdent ident ++ "' must not occur in a "+            ++ "type expression of any class method of this class. "+            ++ violating "class method" (map (unpackIdent . signatureName) ms))++++-- | Checks that no FixedTypeExpression occurs in the given list of named+--   type expressions. The first argument is used in generating a helpful error+--   message and describes what kind of items the second argument contains.++checkNoFixedTEsNamed :: String -> (Identifier, [TypeExpression]) -> ErrorOr ()+checkNoFixedTEsNamed tag (con, ts) =+  let es = mapMaybe checkNoFixedTEsPlain ts+   in errorIf (not . null $ es) $+        pp (head es ++ violating tag [unpackIdent con])++++-- | Checks that no FixedTypeExpression occurs in a type expression.+--   If it does, an error message is created.++checkNoFixedTEs :: TypeExpression -> ErrorOr ()+checkNoFixedTEs t = +  let e = checkNoFixedTEsPlain t+   in errorIf (isJust e) (pp . fromJust $ e)+  +++-- | Returns an error if a FixedTypeExpression occurs in the argument, otherwise+--   returns @Nothing@.++checkNoFixedTEsPlain :: TypeExpression -> Maybe String+checkNoFixedTEsPlain t =+  if (satisfiesSomewhere isFixedTE t)+    then Just "A fixed type expression must not occur in a type expression."+    else Nothing+  where+    isFixedTE t = case t of+      TypeExp _ -> True+      otherwise -> False++++-- | Checks that no function type constructor and no type abstraction+--   constructor occur in the given named list of type expressions.++checkAbsFun :: (Identifier, [TypeExpression]) -> ErrorOr ()+checkAbsFun (con, ts) =+  errorIf (satisfiesSomewhere isAbsOrFun ts) $+    pp ("Algebraic data types and type renamings must be declared without type "+        ++ "abstractions and function type constructors occurring on the "+        ++ "right-hand side."+        ++ violating "data constructor" [unpackIdent con])+  where+    isAbsOrFun t = case t of+      TypeFun _ _   -> True+      TypeAbs _ _ _ -> True+      otherwise     -> False++++++------- Helper functions ------------------------------------------------------+++-- | Applies two functions to a value and creates a pair of the results.++makePair :: (a -> b) -> (a -> c) -> a -> (b, c)+makePair f g x = (f x, g x)+++-- | Creates a list containing just one element.++singletonList :: a -> [a]+singletonList x = [x]++++-- | Filters all elements which occur more than once in the given list.+--   Only one representative is returned for every group of equal items.++extractRepeatingElements :: Ord a => [a] -> [a]+extractRepeatingElements =+  map head . filter (\vs -> length vs > 1) . group . sort++++-- | Tests if a predicate holds somewhere in an arbitrary tree.++satisfiesSomewhere :: (Data a, Data b) => (a -> Bool) -> b -> Bool+satisfiesSomewhere predicate x = everything (||) (False `mkQ` predicate) x+++++

@@ -0,0 +1,130 @@++++-- | Provides error handling functions for checking parser output.+--   The functions and data types of this module are mostly tiny, little+--   helpers used by all parser modules.++module Language.Haskell.FreeTheorems.Frontend.Error where++++import Control.Monad (foldM)+import Control.Monad.Error (Error(..), throwError)+import Control.Monad.Writer (Writer, runWriter, tell)+import Data.List (intersperse)+import Text.PrettyPrint (Doc, empty, text, fsep, ($$), nest)++import Language.Haskell.FreeTheorems.Syntax+    (Declaration, getDeclarationName, unpackIdent)++++-- | A wrapper type for a @Writer@ which stores pretty-printable documents along+--   with checked values.++type Checked a = Writer [Doc] a++++-- | A wrapper type for @Writer@ which stores pretty-printable documents along+--   with parsed values.+--   This type is provided as standard return type for parsers.++type Parsed a = Writer [Doc] a++++++-- | The error type is just a synonym for @Either@ where errors are represented+--   by a pretty-printable @Doc@.++type ErrorOr a = Either Doc a++-- needed to make 'ErrorOr' a monad+instance Error Doc where+  noMsg    = empty+  strMsg s = text s++++-- | A wrapper function for @runWriter@.++runChecks :: Checked a -> (a, [Doc])+runChecks = runWriter++++-- | Applies a checking function (the first argument) element-wise to a list of+--   values (the second argument). The result list contains only those elements+--   for which the checking function does not yield an error.++foldChecks :: (a -> ErrorOr b) -> [a] -> Checked [a]+foldChecks check = foldM doCheck []+  where+    doCheck xs x = +      case getError (check x) of+        Nothing -> return (xs ++ [x])+        Just e  -> tell [e] >> return xs++++-- | Checks if the argument contains an error.++isError :: ErrorOr a -> Bool+isError = either (const True) (const False)++++-- | Returns the error message stored in the argument or @Nothing@ if there is +--   no error message in the argument.++getError :: ErrorOr a -> Maybe Doc+getError = either Just (const Nothing)++++-- | If the first argument is True, then the second argument is taken as an+--   error message. Otherwise () is returned as a non-error message.++errorIf :: Bool -> Doc -> ErrorOr ()+errorIf False = return . const ()+errorIf True  = throwError++++-- | Transforms a string into a pretty-printed document by splitting the string+--   into words and forming a pretty paragraph of all words.++pp :: String -> Doc+pp = fsep . map text . words++++-- | Checks a declaration for errors.+--   If the second argument is an error, this function extends the error +--   message to make clear it belongs to a declaration.++inDecl :: Declaration -> ErrorOr a -> ErrorOr a+inDecl d e = case getError e of+  Nothing  -> e+  Just doc -> throwError $+                pp ("In the declaration of " +                    ++ unpackIdent (getDeclarationName d) ++ ":")+                $$ nest 2 doc+    +++-- | Used to extend error messages by a list of items violating a certain rule. ++violating :: String -> [String] -> String+violating name xs =+  let text = if length xs == 1+               then " The following " ++ name ++ " violates this rule: "+               else " The following " ++ name ++ "s violate this rule: "+   in text ++ (concat . intersperse ", " $ xs)++++

@@ -0,0 +1,302 @@++++-- | Defines standard functions for modifying type expressions or retrieving+--   information from type expressions.++module Language.Haskell.FreeTheorems.Frontend.TypeExpressions (+    freeTypeVariables+  , allTypeVariables+  , createNewTypeVariableNotIn+  , alphaConversion+  , substituteTypeVariables+  , replaceAllTypeSynonyms+  , closeTypeExpressions+  , closureFor+) where++++import Data.Generics+    ( Typeable, Data, synthesize, mkQ, everywhere, mkT, gmapT, GenericQ+    , GenericT )+import Data.List (find)+import Data.Set as Set+    ( Set, empty, union, insert, delete, fold, unions, difference, singleton+    , member )+import Data.Map as Map (Map, empty, lookup, delete, insert)+import Data.Maybe (maybe, fromJust)++import Language.Haskell.FreeTheorems.Syntax+import Language.Haskell.FreeTheorems.NameStores (typeNameStore)++++++------- Functions for type variables ------------------------------------------+++-- | Returns all type variables occurring in a type expression.++allTypeVariables :: TypeExpression -> Set.Set TypeVariable+allTypeVariables = synthesize Set.empty Set.union (id `mkQ` update)+  where+    update t s = case t of+      TypeVar v     -> Set.insert v s+      TypeAbs v _ _ -> Set.insert v s+      otherwise     -> s++++-- | Returns the free type variables of a type expression.++freeTypeVariables :: TypeExpression -> Set.Set TypeVariable+freeTypeVariables = synthesize Set.empty Set.union (id `mkQ` update)+  where+    update t s = case t of+      TypeVar v     -> Set.insert v s+      TypeAbs v _ _ -> Set.delete v s+      otherwise     -> s++++-- | Substitutes every free occurrence of all type variables given in the map+--   with the type expressions they are mapped to.++substituteTypeVariables ::+    Map.Map TypeVariable TypeExpression +    -> TypeExpression +    -> TypeExpression++substituteTypeVariables env t = +  everywhereWith (id `mkQ` update) (mkTw substitute) env t+  where+    -- Updates the environment used in the top-down traversal.+    -- Removes bound type variables from the mapping. Thus, these variables+    -- won't be replaced in the second stage.+    update t env = case t of+      TypeAbs v _ _ -> Map.delete v env+      otherwise     -> env+    +    -- Replaces a type variable by a type expression, if the type variable is+    -- contained in the environment.+    substitute env t = case t of+      TypeVar v -> maybe t id (Map.lookup v env)+      otherwise -> t++++-- | Creates a new type variable not occurring in the given set of type+--   variables.+--+--   A type variable can either be named by the letters \'a\' to \'e\' or, if+--   that causes conflicts, by the letter \'a\' concatenated with a number+--   starting from 1.++createNewTypeVariableNotIn :: Set.Set TypeVariable -> TypeVariable+createNewTypeVariableNotIn forbiddenVars =+  let vars = map (TV . Ident) typeNameStore+   in fromJust $ find (\v -> not (v `Set.member` forbiddenVars)) vars++++-- | Replaces every bound occurrence of the given type variable in the given+--   type expression with a new type variable which is created by+--   'createNewTypeVariableNotIn'.+--+--   Several bound occurrences of the given type variable are replaced with the+--   same new type variable. Only one new type variable is created altogether.++alphaConversion :: TypeVariable -> TypeExpression -> TypeExpression+alphaConversion old t =+  everywhereWith (id `mkQ` change) (mkTw replace) id t+  where+    -- The new type variable which will replace 'old' everywhere in the given+    -- type expression.+    new = createNewTypeVariableNotIn (allTypeVariables t)+    +    -- This function replaces any type variable equal to 'old' with 'new' and+    -- keeps all other type variables unchanged.+    rep v = if (v == old) then new else v++    -- Modifies the function which replaces type variables.+    -- If we are at the type abstraction where 'old' is bound, then 'old' has+    -- to be replaced in every subexpression by the new type variable.+    change t f = case t of+      TypeAbs v _ _ -> if (v == old) then rep else f+      otherwise     -> f++    -- Applies the current replacement function to type variables.+    -- In type abstractions, the static function 'rep' is used to replace+    -- 'old' with 'new' or otherwise keep the type variable.+    -- Note that - independent of the usage of 'rep' - the replacement function+    -- 'r' will be modified by 'change' when advancing to subexpressions.+    replace r t = case t of+      TypeVar v       -> TypeVar (r v)+      TypeAbs v cs t' -> TypeAbs (rep v) cs t'+      otherwise       -> t++++++------- Generic helper definitions --------------------------------------------+++-- | Generic transformations using a value of fixed type.++type GenericTw u = forall a . Data a => u -> a -> a++++-- | Make a generic transformation which uses a value of fixed type.+--   This function takes a specific case into a general case, such that no+--   transformation is applied for types not covered by the specific case.++mkTw :: (Typeable a, Typeable b) => (u -> a -> a) -> u -> b -> b+mkTw f u = mkT $ f u++++-- | Pushes a value in a top-down fashion trough a tree and applies that value+--   from bottom to top to every node.+--+--   More detailed, the expression+--+-- >   everywhereWith update apply v+--+--   is evaluated as follows:+--   The value @v@ is transfered through the tree from top to bottom while,+--   at every node, the function @update@ is applied to it. This allows the+--   initial value to be changed like, for example, an environment gathering+--   information from the root to the leaf while moving through the tree.+--   Thereafter, the transformation function @apply@ is applied to every node+--   from bottom to top. It might use the value distributed to that node.++everywhereWith :: GenericQ (u -> u) -> GenericTw u -> u -> GenericT+everywhereWith k f u x = (f u) $ gmapT (everywhereWith k f (k x u)) x++++++------- Replacing type synonyms -----------------------------------------------+++-- | Replaces all type synonyms in an arbitrary tree.+--   The first argument gives the list of known type synonyms and their +--   declarations. Every occurrence of one of those type synonyms in the second+--   argument is replaced by the according right-hand side of the declaration.+--   +--   Note that the type synonym declarations given in the first argument may+--   themselves contain type synonyms. However, type synonym declarations must+--   not be recursive nor mutually recursive.++replaceAllTypeSynonyms :: (Typeable a, Data a) => [TypeDeclaration] -> a -> a+replaceAllTypeSynonyms knownTypes = everywhere (mkT replace)+    -- This functions replaces all type synonyms in a bottom-up manner.+    -- Thus, when applying 'replace', all type synonyms are already removed+    -- from all children of the node.++  where+    -- Replacing type synonyms only affects type constructors.+    -- Check if there is a type synonym declaration for the given type +    -- constructor. If not, just return the unchanged type expression.+    -- Otherwise replace the type synonym by its definition.+    replace t = case t of+      TypeCon c ts -> maybe t (applyTypeSynonym ts) (findTypeDecl knownTypes c)+      otherwise    -> t++    -- Applies the declaration of a type synonym to a list of type expressions.+    -- The type expression composed in this way is returned.+    -- Note that the structure of 'replaceTypeSynonyms' guarantees that there is+    -- no type synonym in any of the type expressions of 'ts'.+    applyTypeSynonym ts (Type _ vs t) =+      let +          -- First, remove all type synonyms from the declaration's right-hand+          -- side. Note that this terminates because type expressions cannot be+          -- declared recursively nor mutually recursively.+          t1 = replaceAllTypeSynonyms knownTypes t++          -- Construct an environment to be used to substitute every free+          -- variable in 't' by the appropiate type expression of 'ts'.+          env = foldr (uncurry Map.insert) Map.empty (zip vs ts)++          -- Rename all bound variables in 't' such that no free variables of+          -- any type expression in 'ts' will get bound.+          allFreeVariables = Set.unions $ map freeTypeVariables ts+          t2 = Set.fold alphaConversion t1 allFreeVariables++          -- Finally, apply the declaration's right-hand side to 'ts' and return+          -- the constructed type expression.+       in substituteTypeVariables env t2+  +++-- | Looks up the declaration for a type synonym constructor.+--   If the given type constructor is not a type synonym or there is no+--   declaration for this type constructor in the declarations list, then+--   @Nothing@ is returned.++findTypeDecl :: [TypeDeclaration] -> TypeConstructor -> Maybe TypeDeclaration+findTypeDecl decls con = case con of+  Con name  -> find (\d -> typeName d == name) decls +  otherwise -> Nothing++++++------- Closing type expressions ----------------------------------------------+++-- | Closes all type expressions in type signature declarations.+--   Class methods are also modified, in that every free variable expect the+--   class variable is explicitly bound.++closeTypeExpressions :: [Declaration] -> [Declaration]+closeTypeExpressions = map closeDecl+  where+    closeDecl d = case d of+      ClassDecl d -> ClassDecl (closeClassDecl d)+      TypeSig sig -> TypeSig (closeSignature sig)+      otherwise   -> d++++-- | Closes type signatures of class methods. Afterwards, the class variable is+--   still free in all class methods.++closeClassDecl :: ClassDeclaration -> ClassDeclaration+closeClassDecl d =+  d { classFuns = map (closureWithout (classVar d)) (classFuns d) }+  where+    -- Close the class method signature while keeping the class variable free.+    closureWithout v s = +      let t = signatureType s+          freeVars = freeTypeVariables t `Set.difference` Set.singleton v+       in s { signatureType = closureFor freeVars t }++++-- | Close a type signature declaration.++closeSignature :: Signature -> Signature+closeSignature s =+  let t = signatureType s+   in s { signatureType = closureFor (freeTypeVariables t) t }++++-- | Explicitly binds all type variables of the first argument by a type +--   abstraction in the given type expression.++closureFor :: Set.Set TypeVariable -> TypeExpression -> TypeExpression+closureFor vs t = Set.fold (\v -> TypeAbs v []) t vs++++++

@@ -0,0 +1,408 @@++++-- | Declares an intermediate data structure along with a function to transform+--   type signatures into the intermediate structure. There are also other+--   functions working on intermediate structures, namely to retrieve relation+--   variables and to instantiate them to functions.++module Language.Haskell.FreeTheorems.Intermediate (+    Intermediate (..)+  , interpret+  , interpretM+  , relationVariables+  , specialise+  , specialiseInverse+) where++++import Control.Monad (liftM, liftM2, mapM)+import Control.Monad.Reader (ReaderT, ask, runReaderT, local)+import Control.Monad.State (State, get, put, runState)+import Control.Monad.Trans (lift)+import Data.Generics ( Typeable, Data, everywhere, everything, listify, mkT+                     , mkQ, extQ)+import qualified Data.Map as Map (Map, empty, lookup, insert, map)++import Language.Haskell.FreeTheorems.LanguageSubsets+import Language.Haskell.FreeTheorems.Syntax +import Language.Haskell.FreeTheorems.ValidSyntax+import Language.Haskell.FreeTheorems.Theorems+import Language.Haskell.FreeTheorems.Frontend.TypeExpressions+    ( substituteTypeVariables )+import Language.Haskell.FreeTheorems.NameStores +    ( relationNameStore, typeExpressionNameStore, functionNameStore1, functionNameStore2 )+++++------- Intermediate data structure -------------------------------------------+++-- | A structure describing the intermediate result of interpreting a type+--   expression as a relation.++data Intermediate = Intermediate +  { intermediateName      :: String +        -- ^ The name of the symbol for which the theorem is to be generated.+  +  , intermediateSubset    :: LanguageSubset+        -- ^ The language subset in which the theorem is to be generated.+  +  , intermediateRelation :: Relation+        -- ^ The relation obtained from the type.+  +  , functionVariableNames1 :: [String]+        -- ^ A name store for new, fresh function names.+        --   This is needed because functions can be specialised step-by-step+        --   after having generated the first relation from a type.++  , functionVariableNames2 :: [String]+        -- ^ Another name store for new, fresh function names, disjoint from+        --   the one above.++  , signatureNames :: [String]+        -- ^ The names of all known signatures. These names must not be used to+        --   generate names of functions and variables.+  +  , interpretNameStore :: NameStore +        -- ^ A name store to generate new relation variables and type+        --   expressions.+  +  }++++++------- Interpret types as relations ------------------------------------------++++-- | Interprets a valid signature as a relation. This is the key point for+--   generating free theorems.++interpret :: +    [ValidDeclaration] -> LanguageSubset -> ValidSignature -> Maybe Intermediate+interpret vds l s =+  let n  = unpackIdent . signatureName . rawSignature $ s+      ss = getSignatureNames (map rawDeclaration vds)+      fs = n : ss+      t  = signatureType . rawSignature $ s+      (i, rs) = runState (runReaderT (interpretM l t) Map.empty) (initialState fs)+      r = Intermediate n l i (filter (`notElem` fs) functionNameStore1) (filter (`notElem` fs) functionNameStore2) ss rs+   in case l of+        SubsetWithSeq _ -> Just r+        otherwise       -> if containsStrictTypes vds s +                             then Nothing+                             else Just r+  where+    getSignatureNames = everything (++) ([] `mkQ` getSigName)+    getSigName (Signature i _) = [unpackIdent i]++    containsStrictTypes vds s = +      let rs = rawSignature s+          ns = everything (++) ([] `mkQ` getCons `extQ` getClasses) rs+          ds = map (getDeclarationName . rawDeclaration) +                   (filter isStrictDeclaration vds)+          isStrict n = n `elem` ds+       in any isStrict ns++    getCons c = case c of { Con n -> [n] ; otherwise -> [] }+    getClasses (TC n) = [n]++++-- | Transforms a type expression into a relation. The environment is used to+--   map seen type variables to newly created relation variables. The state+--   serves for creating relation variables.++interpretM :: +    LanguageSubset +    -> TypeExpression +    -> ReaderT Environment (State NameStore) Relation++interpretM l t = case t of++    -- get the environment from the reader, lookup the relation variable for+    -- the given type variable (this operation will never fail because+    -- in the initial type expression, all occurring type variables are bound+    -- by type abstraction which are resolved by updating the environment, see+    -- below) and create a relation consisting solely of the relation variable+  TypeVar v -> Map.lookup v =<< ask+  +    -- either create a basic relation or a lift relation, depending on the +    -- subtypes+  TypeCon c ts -> do+    rs <- mapM (interpretM l) ts   -- interpret the subtypes+    ri <- mkRelationInfo l t       -- create the relation info+        +        -- checks if an intermediate relation is a basic case+    let basic rel = case rel of { RelBasic _ -> True ; otherwise -> False }++        -- create a basic intermediate relation if all subrelations are basic+        -- (or if there is no subrelation), otherwise create a lifted relation+    if all basic rs+      then return (RelBasic (RelationInfo l t t))+      else return (RelLift ri c rs)++    -- create a relation for function types+  TypeFun t1 t2 -> do+    ri <- mkRelationInfo l t       -- create the relation info+    liftM2 (RelFun ri) (interpretM l t1) (interpretM l t2)++    -- create a relation for type abstractions+  TypeAbs v cs t' -> do+    ri <- mkRelationInfo l t                    -- create the relation info+    (rv, t1, t2) <- lift newRelationVariable    -- create a new variable+    let rvar = RelVar (RelationInfo l t1 t2) rv+    r  <- local (Map.insert v rvar) $ interpretM l t'  -- subrelations+    let res = relRes l ++ (if null cs then [] else [RespectsClasses cs])+    return (RelAbs ri rv (t1,t2) res r)++  where+    mkRelationInfo l t = do+      env <- ask+        -- create the 'left' and 'right' type expression of 't',+        -- i.e. replace all free variables by the left or right type+        -- expressions of the corresponding relation variable+      let getLt = relationLeftType . relationInfo+      let getRt = relationRightType . relationInfo+      let lt = substituteTypeVariables (Map.map getLt env) t+      let rt = substituteTypeVariables (Map.map getRt env) t+      return (RelationInfo l lt rt)+++    -- Returns the restrictions for relations, depending on the current+    -- language subset and theorem type.+    relRes l = case l of+      BasicSubset                       -> [ ]+      SubsetWithFix EquationalTheorem   -> [ Strict, Continuous ]+      SubsetWithFix InequationalTheorem -> [ Strict, Continuous+                                           , LeftClosed ]+      SubsetWithSeq EquationalTheorem   -> [ Strict, Continuous+                                           , BottomReflecting ]+      SubsetWithSeq InequationalTheorem -> [ Strict, Continuous, Total+                                           , LeftClosed ]+   +++++------- Helper definitions for the interpretation -----------------------------+++-- | An environment mapping type variables to intermediate relation variables+--   (stored as relations).++type Environment = Map.Map TypeVariable Relation ++++-- | Represents the names of future variable names. The first component provides+--   names for relations, while the second component provides names for type+--   expressions.++type NameStore = ([String], [TypeExpression])++++-- | Initialises the name store. Both components of the name store are infinite+--   list.+--   For more information, see 'Language.Haskell.FreeTheorems.NameStore'.++initialState :: [String] -> NameStore+initialState ns = +   ( relationNameStore+   , map (TypeExp . TF . Ident) . filter (`notElem` ns)+         $ typeExpressionNameStore )++++-- | Creates a new relation variable using the name store.++newRelationVariable :: +    State NameStore (RelationVariable, TypeExpression, TypeExpression)+newRelationVariable = do+  (rvs, ts) <- get+  let ([rv], rvs') = splitAt 1 rvs+  let ([t1, t2], ts') = splitAt 2 ts+  put (rvs', ts') +  return (RVar rv, t1, t2)++++++------- Instantiation of relation variables -----------------------------------+++-- | Creates a list of all bound relation variables in an intermediate+--   structure, which can be specialised to a function. ++relationVariables :: Intermediate -> [RelationVariable]+relationVariables (Intermediate _ _ rel _ _ _ _) = getRVar True rel+  where+    getRVar ok rel = case rel of+      RelLift _ _ rs    -> concatMap (getRVar ok) rs+      RelFun _ r1 r2    -> getRVar (not ok) r1 ++ getRVar ok r2+      RelAbs _ rv _ _ r -> (if ok then [rv] else []) ++ getRVar ok r+      FunAbs _ _ _ _ r  -> getRVar ok r +      otherwise         -> []++++-- | Specialises a relation variable to a function variable in an intermediate+--   structure.++specialise :: Intermediate -> RelationVariable -> Intermediate+specialise ir rv = reduceLifts (replaceRelVar ir rv Left)++++-- | Specialises a relation variable to an inverse function variable.+--   This function does not modify intermediate structures in subsets with+--   equational theorems.++specialiseInverse :: Intermediate -> RelationVariable -> Intermediate+specialiseInverse ir rv = +  case theoremType (intermediateSubset ir) of+    EquationalTheorem   -> ir+    InequationalTheorem -> reduceLifts  (replaceRelVar ir rv Right)++++-- | Replaces a relation variable with a function variable.++replaceRelVar :: +    Intermediate -> RelationVariable +    -> (TermVariable -> Either TermVariable TermVariable) -> Intermediate+replaceRelVar ir (RVar rv) leftOrRight =+  let ([funName], fns) = splitAt 1 (functionVariableNames1 ir)+      fv = leftOrRight . TVar $ funName+      relation = intermediateRelation ir+   in ir { intermediateRelation  = everywhere (mkT $ replace rv fv) relation+         , functionVariableNames1 = drop 1 (functionVariableNames1 ir)+         }+  where+    -- perform the actual replacement+    -- when replacing a relation by a 'right' function in a relation+    -- abstraction, the types have to be flipped+    replace rv fv rel = case rel of+      RelVar ri (RVar r) -> +        let tv = either (Left . TermVar) (Right . TermVar) fv+         in if rv == r then FunVar ri tv else rel+      RelAbs ri (RVar r) ts res rel' ->+        let res' = either (const funResL) (const funResR) fv+         in if rv == r+              then FunAbs ri fv ts (res' ++ (classConstraints res)) rel'+              else rel+      otherwise -> rel++    -- the restrictions for functions in the equational setting and for+    -- 'left' functions in inequational settings+    funResL = case intermediateSubset ir of+      BasicSubset     -> [ ]+      SubsetWithFix _ -> [ Strict ]+      SubsetWithSeq _ -> [ Strict, Total ]+    +    -- the restrictions for 'right' functions in the inequational settings+    funResR = case intermediateSubset ir of+      BasicSubset     -> [ ]+      SubsetWithFix _ -> [ ]+      SubsetWithSeq _ -> [ Strict ]++    -- returns the class constraints+    classConstraints res = filter isCC res+      where +        isCC r = case r of { RespectsClasses _ -> True ; otherwise -> False }++++-- | Applies simplifications on lifted constructors. +--   If the argument is a function then lifted lists are replaced by map and+--   lifted Maybes are replaced by fmap.++reduceLifts :: Intermediate -> Intermediate+reduceLifts ir = +--  ir { intermediateRelation = reduceEverywhere (intermediateRelation ir) }+  ir { intermediateRelation = re True (intermediateRelation ir) }+  where+--    reduceEverywhere = everywhere (mkT reduce)++    re ok rel = case rel of+      RelLift ri con rs     -> if ok +                                 then reduce (RelLift ri con (map (re ok) rs))+                                 else rel+      RelFun ri r1 r2       -> RelFun ri (re (mk' (not ok) ri r1) r1) +                                         (re (mk ok ri r2) r2)+      RelAbs ri rv ts res r -> RelAbs ri rv ts res (re ok r)+      FunAbs ri fv ts res r -> FunAbs ri fv ts res (re ok r)+      otherwise             -> rel++    mk' ok ri r = case theoremType (relationLanguageSubset ri) of+                    EquationalTheorem   -> True+                    InequationalTheorem -> +                      case r of+                        RelLift _ ConList _ -> True+                        otherwise           -> ok+++    mk ok ri r = case theoremType (relationLanguageSubset ri) of+                   EquationalTheorem   -> True+                   InequationalTheorem -> ok+++    -- Transforms a lifted constructor to a function, if possible.+    -- This function is applied in a bottom-up manner, therefore the+    -- arguments of the lifted constructor are already reduced.+    reduce rel = case rel of+      RelLift ri con rs -> maybe rel id (toTerm ri con rs)+      otherwise         -> rel++    -- Tries to transform a lifted relation. If not succesful, Nothing is+    -- returned.+    toTerm ri con rs = do+      f <- funSymbol con+      -- first check if all arguments are 'left' functions+      case mapM leftFun rs of+        Just fts -> Just . FunVar ri . Left $ term f fts+        Nothing  -> -- then check if all arguments are 'right' functions+                    case mapM rightFun rs of+                      Just fts -> Just . FunVar ri . Right $ term f fts+                      Nothing  -> Nothing++    -- Returns the function symbol associated with a lifted constructor.+    funSymbol con = case con of+      ConList             -> Just . TVar $ "map"+      Con (Ident "Maybe") -> Just . TVar $ "fmap"+      otherwise           -> Nothing++    -- Checks if 'rel' is a 'left' function. If so, its term and type is+    -- returned, otherwise Nothing.+    leftFun rel = case rel of+      FunVar ri (Left f) -> Just (f, ( relationLeftType ri+                                     , relationRightType ri))+      otherwise          -> Nothing++    -- Checks if 'rel' is a 'right' function. If so, its term and type is+    -- returned, otherwise Nothing.+    -- The returned type is flipped mirroring the fact that right functions are+    -- actually inverse functions.+    rightFun rel = case rel of+      FunVar ri (Right f) -> Just (f, ( relationRightType ri+                                      , relationLeftType ri))+      otherwise           -> Nothing++    -- Creates a term by instantiating 'f' and applying the arguments of 'fts'.+    term f fts = +        let (fs, ts) = unzip fts+            termins t (t1, t2) = TermIns (TermIns t t1) t2+         in foldl TermApp (foldl termins (TermVar f) ts) fs+      +++++

@@ -0,0 +1,59 @@+++-- | Declares the available Haskell language subsets and the result types for+--   generating free theorems. ++module Language.Haskell.FreeTheorems.LanguageSubsets where++++import Data.Generics (Typeable, Data)++++-- | Descriptions of the Haskell language subsets for which free theorems can+--   be generated.++data LanguageSubset+  = BasicSubset+        -- ^ This subset describes only terms in which no undefinedness may.+        --   This excludes terms defined using general recursion or selective+        --   strictness (as offered by @seq@).++  | SubsetWithFix TheoremType+        -- ^ This subset describes terms in which undefined values may occur+        --   such as introduced by a fixpoint combinator or possibly failing+        --   pattern matches (if not all cases are covered).+        --   This excludes any term based on @seq@.++  | SubsetWithSeq TheoremType+        -- ^ Additionally to the fix subset, this subset allows terms to+        --   be defined using @seq@.++  deriving (Typeable, Data, Eq)++++-- | Returns the theorem type for a given language subset.++theoremType :: LanguageSubset -> TheoremType+theoremType l = case l of+  BasicSubset     -> EquationalTheorem+  SubsetWithFix t -> t+  SubsetWithSeq t -> t++++-- | The result type for generating free theorems.++data TheoremType+  = EquationalTheorem+        -- ^ An equational free theorem should be generated.++  | InequationalTheorem+        -- ^ Two inequational free theorems should be generated.++  deriving (Typeable, Data, Eq)+++

@@ -0,0 +1,65 @@++++-- | Provides functions to generate new variable names of different kinds.++module Language.Haskell.FreeTheorems.NameStores where++++import Data.List (unfoldr)++++-- | An infinite list of names for type variables.++typeNameStore :: [String]+typeNameStore = createNames "abcde" 'a'++++-- | An infinite list of names for relation variables.++relationNameStore :: [String]+relationNameStore = createNames "RS" 'R'++++-- | An infinite list of names for type expressions.++typeExpressionNameStore :: [String]+typeExpressionNameStore = createNames "" 't'++++-- | An infinite list of names for function variables.++functionNameStore1 :: [String]+functionNameStore1 = createNames "fgh" 'f'+++-- | Another infinite list of names for function variables.++functionNameStore2 :: [String]+functionNameStore2 = createNames "pqrs" 'p'++++-- | An infinite list of names for term variables.++variableNameStore :: [String]+variableNameStore = createNames "xyzvwabcdeijklmn" 'x'++++-- | Creates an infinite list of names based on a list of simple names and a+--   default prefix. After simple names have been used, the numbers starting+--   from 1 are appended to the default prefix to generate more names.++createNames :: [Char] -> Char -> [String]+createNames prefixes prefix =+  let unpack is = case is of { (c:cs) -> Just ([c], cs) ; otherwise -> Nothing }+   in unfoldr unpack prefixes ++ (map (\i -> prefix : show i) [1..])+++

@@ -0,0 +1,472 @@++++-- | Defines a function to parse a string into a list of declarations.+--   This module is based on the \'haskell-src\' package most probably included+--   with every Haskell compiler.++module Language.Haskell.FreeTheorems.Parser.Haskell98 (parse) where++++import Control.Monad (foldM, liftM, liftM2)+import Control.Monad.Error (throwError)+import Control.Monad.Writer (Writer, tell)+import Data.Generics (everywhere, mkT)+import Data.List (nub)+import Language.Haskell.Parser (parseModule, ParseResult(..))+import Language.Haskell.Syntax+import Text.PrettyPrint++import qualified Language.Haskell.FreeTheorems.Syntax as S+import Language.Haskell.FreeTheorems.Frontend.Error+++++------- Main parser function --------------------------------------------------+++-- | Parses a string to a list of declarations.+--   The string should contain a Haskell module.+--+--   This function is based on the Haskell98 parser of the \'haskell-src\'+--   package, i.e. the module \'Language.Haskell.Parser\'.+--   That parser supports only Haskell98 and a few extensions. Especially, it+--   does not support explicit quantification of type variables and thus no +--   higher-rank functions.+--+--   The declarations returned by 'parse' include only @type@, @data@, +--   @newtype@, @class@ and type signature declarations.+--   All other declarations and syntactical elements in the input are ignored.+--   +--   Furthermore, the following restrictions apply:+--+--   * Multi-parameter type classes are not allowed and therefore ignored. When+--     declaring a type class, the argument to the type class name must be a+--     single type variable.+--+--   * A type variable must not be applied to any type. That means, for+--     example, that the type @m a@ is not accepted.+--+--   * Contexts and @deriving@ parts in @data@ and @newtype@ declarations+--     are ignored.+--+--   * The module names are ignored. If any identifier was given qualified, the+--     module part of a qualified name is ignored.+--   +--   * Special Haskell constructors (unit, list function) are not allowed as+--     identifiers.+--+--   If a parser error occurs, as suitable error message is returned in the+--   second component of the returned tuple and the first component will be the+--   empty list.+--   However, if parsing was successful, but the parsed structures could not+--   be completely transformed into @Declaration@s, suitable transformation+--   error messages are returned in the second component while the first+--   components contains all declarations which could be transformed+--   successfully.++parse :: String -> Parsed [S.Declaration]+parse text = case parseModule text of+  ParseOk hsModule -> let decls = transform . filterDeclarations $ hsModule+                       in foldM collectDeclarations [] decls+  ParseFailed l _  -> do tell [pp ("Parse error at (" ++ show (srcLine l)+                                   ++ ":" ++ show (srcColumn l) ++ ").")]+                         return []+  where+    collectDeclarations :: [S.Declaration] -> HsDecl -> Parsed [S.Declaration]+    collectDeclarations ds d = +      case mkDeclaration d of+        Left e   -> tell [e] >> return ds+        Right d' -> return (ds ++ [d'])+      +++++------- Filter declarations ---------------------------------------------------++++-- | Filters all declarations of a Haskell module.++filterDeclarations :: HsModule -> [HsDecl]+filterDeclarations (HsModule _ _ _ _ ds) = filter isAcceptedDeclaration ds+  where+    isAcceptedDeclaration decl = case decl of+      HsTypeDecl _ _ _ _        -> True+      HsDataDecl _ _ _ _ _ _    -> True+      HsNewTypeDecl _ _ _ _ _ _ -> True+      HsClassDecl _ _ _ _ _     -> True+      HsTypeSig _ _ _           -> True+      otherwise                 -> False++++-- | Transforms a list of declarations by simplifying type signatures.++transform :: [HsDecl] -> [HsDecl]+transform = everywhere (mkT extendTypeSignature)+  where+    -- Type signatures can be given for several names at once.+    -- This function transforms declarations such that every type signature is+    -- given for exactly one name only.+    extendTypeSignature :: [HsDecl] -> [HsDecl]+    extendTypeSignature ds = case ds of+      ((HsTypeSig l ns t):ds') -> (map (\n -> HsTypeSig l [n] t) ns) ++ ds'+      otherwise                -> ds++++++------- Transform declarations ------------------------------------------------++++-- | Transforms a declaration.++mkDeclaration :: HsDecl -> ErrorOr S.Declaration+mkDeclaration decl = case decl of+  HsTypeDecl l n vs t               -> addErr l n (mkType n vs t)+  HsDataDecl l _ n vs cs _          -> addErr l n (mkData n vs cs)+  HsNewTypeDecl l _ n vs c _        -> addErr l n (mkNewtype n vs c)+  HsClassDecl l scs n [v] ds        -> addErr l n (mkClass scs n v ds)+  HsTypeSig l [n] (HsQualType cx t) -> addErr l n (mkSignature cx n t)++  HsClassDecl l _ n [] _      -> addErr l n (throwError missingVar)+  HsClassDecl l _ n (_:_:_) _ -> addErr l n (throwError noMultiParam)++  -- no other case con occur, see above function 'filterDeclarations'. +++missingVar   = pp "Missing type variable to be constrained by type class."+noMultiParam = pp "Multi-parameter type classes are not allowed."++++-- | Adds an error message based on the name of a declaration if the given+--   transformation caused an error.++addErr :: SrcLoc -> HsName -> ErrorOr S.Declaration-> ErrorOr S.Declaration+addErr loc name e = case getError e of+  Nothing  -> e+  Just doc -> throwError $+                pp ("In the declaration of `" ++ hsNameToString name +                    ++ "' at (" ++ show (srcLine loc) ++ ":"+                    ++ show (srcColumn loc) ++ "):")+                $$ nest 2 doc++++-- | Transforms the components of a type declaration.++mkType :: HsName -> [HsName] -> HsType -> ErrorOr S.Declaration+mkType name vars ty = do+  ident <- mkIdentifier name+  tvs   <- mapM mkTypeVariable vars+  t     <- mkTypeExpression ty+  return (S.TypeDecl (S.Type ident tvs t))++++-- | Transforms the components of a data declaration.++mkData :: HsName -> [HsName] -> [HsConDecl] -> ErrorOr S.Declaration+mkData name vars cons = do+  ident <- mkIdentifier name+  tvs   <- mapM mkTypeVariable vars+  ds    <- mapM mkDataConstructorDeclaration cons+  return (S.DataDecl (S.Data ident tvs ds))+       +++-- | Transforms a data constructor declaration.++mkDataConstructorDeclaration :: +    HsConDecl -> ErrorOr S.DataConstructorDeclaration++mkDataConstructorDeclaration (HsConDecl _ name btys) = mkDataConDecl name btys++mkDataConstructorDeclaration (HsRecDecl _ name rbtys) = +  let btys = concatMap (\(l,ty) -> replicate (length l) ty) rbtys+   in mkDataConDecl name btys+  +++-- | Transforms the components of a data constructor declaration.++mkDataConDecl ::+    HsName -> [HsBangType] -> ErrorOr S.DataConstructorDeclaration++mkDataConDecl name btys = do+  ident <- mkIdentifier name+  bts   <- mapM mkBangTyEx btys+  return (S.DataCon ident bts)+  where+    mkBangTyEx (HsBangedTy ty)   = liftM S.Banged   (mkTypeExpression ty)+    mkBangTyEx (HsUnBangedTy ty) = liftM S.Unbanged (mkTypeExpression ty)++++-- | Transforms the components of a newtype declaration.++mkNewtype :: HsName -> [HsName] -> HsConDecl -> ErrorOr S.Declaration+mkNewtype name vars con = do+  ident   <- mkIdentifier name+  tvs     <- mapM mkTypeVariable vars+  (con,t) <- mkNewtypeConDecl con+  return (S.NewtypeDecl (S.Newtype ident tvs con t))+  where+    mkNewtypeConDecl (HsConDecl _ c bts) = mkNCD c bts+    mkNewtypeConDecl (HsRecDecl _ c bts) = mkNCD c (snd $ unzip bts)++    mkNCD c [bty] = liftM2 (,) (mkIdentifier c) (bang bty)+    mkNCD c []      = throwError errNewtype+    mkNCD c (_:_:_) = throwError errNewtype++    errNewtype = +      pp "A `newtype' declaration must have exactly one type expression."++    bang (HsUnBangedTy ty) = mkTypeExpression ty+    bang (HsBangedTy ty)   = +      throwError (pp "A `newtype' declaration must not use a strictness flag.")++++-- | Transforms the components of a Haskell class declaration.+--   Every declaration in the class body is ignored except of type signatures.++mkClass :: HsContext -> HsName -> HsName -> [HsDecl] -> ErrorOr S.Declaration+mkClass ctx name var decls = do+  ident   <- mkIdentifier name+  tv      <- mkTypeVariable var+  superCs <- mkContext ctx >>= check tv+  sigs    <- liftM (map toSig) (mapM mkDeclaration (filter isSig decls))+    -- mapping 'isSig' is safe because after applying 'filter' no other+    -- declarations are left except of type signatures++  return (S.ClassDecl (S.Class superCs ident tv sigs))+  where+    -- Returns 'True' if a declaration is a type signature, otherwise 'False'.+    isSig :: HsDecl -> Bool+    isSig decl = case decl of+      HsTypeSig _ _ _ -> True+      otherwise       -> False++    -- Extracts a signature from a declaration.+    -- Note that no other has to be given here because all declarations passed+    -- as argument to this function are definitely type signatures.+    -- See application of 'isSig' above.+    toSig :: S.Declaration -> S.Signature+    toSig (S.TypeSig s) = s++    -- Checks if only the given type variable occurs in the second parameter.+    -- If not, an error is returned, otherwise, the list of type classes is+    -- extracted.+    check :: +        S.TypeVariable +        -> [(S.TypeClass, S.TypeVariable)] +        -> ErrorOr [S.TypeClass]+    check tv@(S.TV (S.Ident v)) ctx =+      let (tcs, tvs) = unzip ctx+       in if null (filter (/= tv) tvs)+        then return tcs+        else throwError (errClass v)++    errClass v = +      pp $ "Only `" ++ v ++ "' can be constrained by the superclasses."++++-- | Transforms the components of a Haskell type signature.+--   The context is added to the type expression.++mkSignature :: HsContext -> HsName -> HsType -> ErrorOr S.Declaration+mkSignature ctx var ty = do+  context <- mkContext ctx+  ident   <- mkIdentifier var+  t       <- mkTypeExpression ty+  return $ S.TypeSig (S.Signature ident (merge context t))+  where+    -- Merges the context and the type expression. The context is represented+    -- as type abstractions.+    merge :: +        [(S.TypeClass, S.TypeVariable)] +        -> S.TypeExpression +        -> S.TypeExpression+    merge ctx t =+      let -- All variables occurring in a context.+          vars      = (nub . snd . unzip) ctx+          -- Returns all classes associated to a type variable 'v' in 'ctx'.+          classes v = map fst (filter ((==) v . snd) ctx)+       in foldr (\v -> S.TypeAbs v (classes v)) t vars++++-- | Transforms a Haskell context.+--   If the context contains not only variables, but also more complex types,+--   this function fails with an appropriate error message.++mkContext :: HsContext -> ErrorOr [(S.TypeClass, S.TypeVariable)]+mkContext = mapM trans+  where+    trans (qname, tys) = case tys of+      [HsTyVar var] -> do ident <- liftM S.TC (mkIdentifierQ qname)+                          tv    <- mkTypeVariable var+                          return $ (ident, tv)+      otherwise     -> throwError errContext++errContext =+  pp "Only a type variable may be constrained by a class in a context."++++++------- Transform type expressions --------------------------------------------++++-- | Transforms a Haskell type.+--   Note that a type variable is not allowed to be applied to some type.++mkTypeExpression :: HsType -> ErrorOr S.TypeExpression+mkTypeExpression (HsTyVar var)     = liftM S.TypeVar (mkTypeVariable var)+mkTypeExpression (HsTyApp ty1 ty2) = mkAppTyEx ty1 [ty2]+mkTypeExpression (HsTyCon qname)   = mkTypeConstructorApp qname []++mkTypeExpression (HsTyFun ty1 ty2) = do+  t1 <- mkTypeExpression ty1+  t2 <- mkTypeExpression ty2+  return (S.TypeFun t1 t2)++mkTypeExpression (HsTyTuple tys)   = do+  ts <- mapM mkTypeExpression tys+  return (S.TypeCon (S.ConTuple (length ts)) ts)+++++-- | Collects applied types and transforms them into a type expression.++mkAppTyEx :: HsType -> [HsType] -> ErrorOr S.TypeExpression+mkAppTyEx ty tys = case ty of+  HsTyFun _ _   -> throwError $ pp ("A function type must not be applied to a "+                                    ++ "type.")+  HsTyTuple _   -> throwError (pp "A tuple type must not be applied to a type.")+  HsTyVar _     -> throwError (pp "A variable must not be applied to a type.")+  HsTyApp t1 t2 -> mkAppTyEx t1 (t2 : tys)+  HsTyCon qname -> mapM mkTypeExpression tys >>= mkTypeConstructorApp qname ++++-- | Interprets a qualified name as a type constructor and applies it to a list+--   of type expressions.+--   The function type constructor is handled specially because it has to have+--   exactly two arguments.++mkTypeConstructorApp :: +    HsQName +    -> [S.TypeExpression] +    -> ErrorOr S.TypeExpression++mkTypeConstructorApp (Special HsFunCon) [t1,t2] = return $ S.TypeFun t1 t2+mkTypeConstructorApp (Special HsFunCon) _       = throwError errorTypeConstructorApp++mkTypeConstructorApp qname              ts      = +  liftM (\con -> S.TypeCon con ts) (mkTypeConstructor qname)++errorTypeConstructorApp =+  pp "The function type constructor `->' must be applied to exactly two types."++++-- | Transforms a qualified name into a type constructor.+--   Special care is taken for primitive types which could be qualified by+--   \'Prelude\'.++mkTypeConstructor :: HsQName -> ErrorOr S.TypeConstructor+mkTypeConstructor (Qual (Module mod) hsName) = +  if mod == "Prelude"+    then return (asCon hsName)+    else return (S.Con $ hsNameToIdentifier hsName)+mkTypeConstructor (UnQual hsName)          = return $ asCon hsName+mkTypeConstructor (Special HsUnitCon)      = return $ S.ConUnit+mkTypeConstructor (Special HsListCon)      = return $ S.ConList+mkTypeConstructor (Special (HsTupleCon n)) = return $ S.ConTuple n++-- missing case '(Special HsFunCon)' cannot occur,+-- see function 'mkTypeCOnstructorApp'++-- missing case '(Special HsCons)' cannot occur,+-- this is not valid Haskell syntax++++-- | Transforms a name into a type constructor. This functions differentiates+--   between primitive types and other types.++asCon :: HsName -> S.TypeConstructor+asCon name = case name of+  HsIdent "Int"     -> S.ConInt+  HsIdent "Integer" -> S.ConInteger+  HsIdent "Float"   -> S.ConFloat+  HsIdent "Double"  -> S.ConDouble+  HsIdent "Char"    -> S.ConChar+  otherwise         -> S.Con $ hsNameToIdentifier name++++-- | Transforms a Haskell name into a type variable.++mkTypeVariable :: HsName -> ErrorOr S.TypeVariable+mkTypeVariable = return . S.TV . hsNameToIdentifier++++-- | Transforms a qualified Haskell name into an identifier.+--   The module part of a qualified name is ignored.+--   This function fails with an appropriate error message when applied to a+--   special Haskell constructor, i.e. a unit, list, function or tuple+--   constructor.++mkIdentifierQ :: HsQName -> ErrorOr S.Identifier+mkIdentifierQ (UnQual hsName)          = return (hsNameToIdentifier hsName)+mkIdentifierQ (Qual (Module _) hsName) = return (hsNameToIdentifier hsName)++mkIdentifierQ (Special HsUnitCon)      = throwErrorIdentifierQ "`()'"+mkIdentifierQ (Special HsListCon)      = throwErrorIdentifierQ "`[]'"+mkIdentifierQ (Special HsFunCon)       = throwErrorIdentifierQ "`->'"+mkIdentifierQ (Special HsCons)         = throwErrorIdentifierQ "`:'"+mkIdentifierQ (Special (HsTupleCon _)) = throwErrorIdentifierQ "for tuples"++throwErrorIdentifierQ s = throwError $ pp $+  "The constructor " ++ s ++ " must not be used as an identifier."++++-- | Transforms a Haskell name into an identifier.+--   This function encapsulates 'hsNameToIdentifier' into the 'ErrorOr' monad.++mkIdentifier :: HsName -> ErrorOr S.Identifier+mkIdentifier = return . hsNameToIdentifier++++-- | Transforms a Haskell name into an identifier.++hsNameToIdentifier :: HsName -> S.Identifier+hsNameToIdentifier = S.Ident . hsNameToString++++-- | Transforms a Haskell name into a string.+--   Haskell symbols are surrounded by parentheses.++hsNameToString :: HsName -> String+hsNameToString (HsIdent s)  = s+hsNameToString (HsSymbol s) = "(" ++ s ++ ")"++

@@ -0,0 +1,528 @@+++module Language.Haskell.FreeTheorems.Parser.Hsx (parse) where++++import Control.Monad (foldM, liftM, liftM2, when)+import Control.Monad.Error (Error (..), throwError)+import Control.Monad.Reader (ReaderT, runReaderT, local, ask)+import Control.Monad.Trans (lift)+import Control.Monad.Writer (Writer, tell)+import Data.Generics (everywhere, mkT)+import Data.Maybe (fromMaybe)+import Data.List (nub, (\\), intersect)+import Language.Haskell.Hsx.Parser (parseModule, ParseResult(..))+import Language.Haskell.Hsx.Syntax+import Text.PrettyPrint++import qualified Language.Haskell.FreeTheorems.Syntax as S+import Language.Haskell.FreeTheorems.Frontend.Error+++++------- Main parser function --------------------------------------------------+++-- | Parses a string to a list of declarations.+--   The string should contain a Haskell module.+--+--   This function is based on the extended Haskell parser of the +--   \'haskell-src-exts\' package.+--+--   The declarations returned by 'parse' include only @type@, @data@, +--   @newtype@, @class@ and type signature declarations.+--   All other declarations and syntactical elements in the input are ignored.+--   +--   Furthermore, the following restrictions apply:+--+--   * Multi-parameter type classes are not allowed and therefore ignored. When+--     declaring a type class, the argument to the type class name must be a+--     single type variable.+--+--   * Only type variables can be constrained by type classes. That means, for+--     example, the type @Eq [a] => [a]@ is not accepted.+--+--   * A type variable must not be applied to any type. That means, for+--     example, that the type @m a@ is not accepted.+--+--   * Contexts and @deriving@ parts in @data@ and @newtype@ declarations+--     are ignored.+--+--   * The module names are ignored. If any identifier was given qualified, the+--     module part of a qualified name is ignored.+--   +--   * Special Haskell constructors (unit, list function) are not allowed as+--     identifiers.+--+--   * Further extensions over Haskell98 allowed by the underlying parser are+--     also forbidden, namely generalised algebraic data types and unboxed +--     tuples.+--+--   If a parser error occurs, as suitable error message is returned in the+--   second component of the returned tuple and the first component will be the+--   empty list.+--   However, if parsing was successful, but the parsed structures could not+--   be completely transformed into @Declaration@s, suitable transformation+--   error messages are returned in the second component while the first+--   components contains all declarations which could be transformed+--   successfully.++parse :: String -> Parsed [S.Declaration]+parse text = case parseModule text of+  ParseOk hsModule -> let decls = transform . filterDeclarations $ hsModule+                       in foldM collectDeclarations [] decls+  ParseFailed l _  -> do tell [pp ("Parse error at (" ++ show (srcLine l)+                                   ++ ":" ++ show (srcColumn l) ++ ").")]+                         return []+  where+    collectDeclarations :: [S.Declaration] -> HsDecl -> Parsed [S.Declaration]+    collectDeclarations ds d = +      case mkDeclaration d of+        Left e   -> tell [e] >> return ds+        Right d' -> return (ds ++ [d'])+      +++++------- Filter declarations ---------------------------------------------------++++-- | Filters all declarations of a Haskell module.++filterDeclarations :: HsModule -> [HsDecl]+filterDeclarations (HsModule _ _ _ _ ds) = filter isAcceptedDeclaration ds+  where+    isAcceptedDeclaration decl = case decl of+      HsTypeDecl _ _ _ _        -> True+      HsDataDecl _ _ _ _ _ _    -> True+      HsNewTypeDecl _ _ _ _ _ _ -> True+      HsClassDecl _ _ _ _ _ _   -> True+      HsTypeSig _ _ _           -> True+      otherwise                 -> False++++-- | Transforms a list of declarations by simplifying type signatures.++transform :: [HsDecl] -> [HsDecl]+transform = everywhere (mkT extendTypeSignature)+  where+    -- Type signatures can be given for several names at once.+    -- This function transforms declarations such that every type signature is+    -- given for exactly one name only.+    extendTypeSignature :: [HsDecl] -> [HsDecl]+    extendTypeSignature ds = case ds of+      ((HsTypeSig l ns t):ds') -> (map (\n -> HsTypeSig l [n] t) ns) ++ ds'+      otherwise                -> ds++++++------- Transform declarations ------------------------------------------------+++-- | Transforms a declaration.++mkDeclaration :: HsDecl -> ErrorOr S.Declaration+mkDeclaration decl = case decl of+  HsTypeDecl l n vs t           -> addErr l n (mkType n vs t)+  HsDataDecl l _ n vs cs _      -> addErr l n (mkData n vs cs)+  HsNewTypeDecl l _ n vs c _    -> addErr l n (mkNewtype n vs c)+  HsClassDecl l scs n [v] _ ds  -> addErr l n (mkClass scs n v ds)+  HsTypeSig l [n] t             -> addErr l n (mkSignature n t)++  HsClassDecl l _ n [] _ _      -> addErr l n (throwError missingVar)+  HsClassDecl l _ n (_:_:_) _ _ -> addErr l n (throwError noMultiParam)++  -- no other case con occur, see above function 'filterDeclarations'. +++missingVar   = pp "Missing type variable to be constrained by the type class."+noMultiParam = pp "Multi-parameter type classes are not allowed."++++-- | Adds an error message based on the name of a declaration if the given+--   transformation caused an error.++addErr :: SrcLoc -> HsName -> ErrorOr S.Declaration-> ErrorOr S.Declaration+addErr loc name e = case getError e of+  Nothing  -> e+  Just doc -> throwError $+                pp ("In the declaration of `" ++ hsNameToString name +                    ++ "' at (" ++ show (srcLine loc) ++ ":" +                    ++ show (srcColumn loc) ++ "):")+                $$ nest 2 doc++++-- | Transforms the components of a type declaration.++mkType :: HsName -> [HsName] -> HsType -> ErrorOr S.Declaration+mkType name vars ty = do+  ident <- mkIdentifier name+  tvs   <- mapM mkTypeVariable vars+  t     <- mkTypeExpression ty+  return (S.TypeDecl (S.Type ident tvs t))++++-- | Transforms the components of a data declaration.++mkData :: HsName -> [HsName] -> [HsQualConDecl] -> ErrorOr S.Declaration+mkData name vars cons = do+  ident <- mkIdentifier name+  tvs   <- mapM mkTypeVariable vars+  ds    <- mapM mkDataConstructorDeclaration cons+  return (S.DataDecl (S.Data ident tvs ds))+       +++-- | Transforms a data constructor declaration.++mkDataConstructorDeclaration :: +    HsQualConDecl -> ErrorOr S.DataConstructorDeclaration++mkDataConstructorDeclaration (HsQualConDecl _ _ _ (HsConDecl name btys)) =+  mkDataConDecl name btys++mkDataConstructorDeclaration (HsQualConDecl _ _ _ (HsRecDecl name rbtys)) =+  let btys = concatMap (\(l,ty) -> replicate (length l) ty) rbtys+   in mkDataConDecl name btys+  +++-- | Transforms the components of a data constructor declaration.++mkDataConDecl ::+    HsName +    -> [HsBangType] +    -> ErrorOr S.DataConstructorDeclaration++mkDataConDecl name btys = do+  ident <- mkIdentifier name+  bts   <- mapM mkBangTyEx btys+  return (S.DataCon ident bts)+  where+    mkBangTyEx (HsBangedTy ty)   = liftM S.Banged   (mkTypeExpression ty)+    mkBangTyEx (HsUnBangedTy ty) = liftM S.Unbanged (mkTypeExpression ty)++++-- | Transforms the components of a newtype declaration.++mkNewtype :: HsName -> [HsName] -> HsQualConDecl -> ErrorOr S.Declaration+mkNewtype name vars (HsQualConDecl _ _ _ con) = do+  ident   <- mkIdentifier name+  tvs     <- mapM mkTypeVariable vars+  (con,t) <- mkNewtypeConDecl con+  return (S.NewtypeDecl (S.Newtype ident tvs con t))+  where+    mkNewtypeConDecl (HsConDecl c bts) = mkNCD c bts+    mkNewtypeConDecl (HsRecDecl c bts) = mkNCD c (snd $ unzip bts)++    mkNCD c [bty] = liftM2 (,) (mkIdentifier c) (bang bty)+    mkNCD c []      = throwError errNewtype+    mkNCD c (_:_:_) = throwError errNewtype++    errNewtype = +      pp "A `newtype' declaration must have exactly one type expression."++    bang (HsUnBangedTy ty) = mkTypeExpression ty+    bang (HsBangedTy ty)   = +      throwError (pp "A `newtype' declaration must not use a strictness flag.")++++-- | Transforms the components of a Haskell class declaration.+--   Every declaration in the class body is ignored except of type signatures.++mkClass :: HsContext -> HsName -> HsName -> [HsDecl] -> ErrorOr S.Declaration+mkClass ctx name var decls = do+  ident   <- mkIdentifier name+  tv      <- mkTypeVariable var+  superCs <- mkContext ctx >>= check tv+  sigs    <- liftM (map toSig) (mapM mkDeclaration (filter isSig decls))+    -- mapping 'isSig' is safe because after applying 'filter' no other+    -- declarations are left except of type signatures++  return (S.ClassDecl (S.Class superCs ident tv sigs))+  where+    -- Returns 'True' if a declaration is a type signature, otherwise 'False'.+    isSig :: HsDecl -> Bool+    isSig decl = case decl of+      HsTypeSig _ _ _ -> True+      otherwise       -> False++    -- Extracts a signature from a declaration.+    -- Note that no other has to be given here because all declarations passed+    -- as argument to this function are definitely type signatures.+    -- See application of 'isSig' above.+    toSig :: S.Declaration -> S.Signature+    toSig (S.TypeSig s) = s++    -- Checks if only the given type variable occurs in the second parameter.+    -- If not, an error is returned, otherwise, the list of type classes is+    -- extracted.+    check :: +        S.TypeVariable +        -> [(S.TypeClass, S.TypeVariable)] +        -> ErrorOr [S.TypeClass]+    check tv@(S.TV (S.Ident v)) ctx =+      let (tcs, tvs) = unzip ctx+       in if null (filter (/= tv) tvs)+        then return tcs+        else throwError (errClass v)++    errClass v = +      pp $ "Only `" ++ v ++ "' can be constrained by the superclasses."++++-- | Transforms the components of a Haskell type signature.+--   The context is added to the type expression.++mkSignature :: HsName -> HsType -> ErrorOr S.Declaration+mkSignature var ty = do+  ident   <- mkIdentifier var+  t       <- mkTypeExpression ty+  return $ S.TypeSig (S.Signature ident t)++++-- | Transforms a Haskell context.+--   If the context contains not only variables, but also more complex types,+--   this function fails with an appropriate error message.++mkContext :: HsContext -> ErrorOr [(S.TypeClass, S.TypeVariable)]+mkContext = mapM trans+  where+    trans (HsClassA qname [HsTyVar var]) = do+      ident <- liftM S.TC (mkIdentifierQ qname)+      tv    <- mkTypeVariable var+      return $ (ident, tv) +    +    trans (HsClassA _ _) = throwError errContext+    trans (HsIParam _ _) = throwError errImplicit++errContext =+  pp "Only a type variable may be constrained by a class in a context."++errImplicit = +  pp "Implicit parameters are not allowed." +++++------- Transform type expressions --------------------------------------------++++type EnvErrorOr a = ReaderT [S.TypeVariable] (Either Doc) a++++mkTypeExpression :: HsType -> ErrorOr S.TypeExpression+mkTypeExpression ty = runReaderT (mkTypeExpressionT ty) []++++-- | Transforms a Haskell type.+--   Note that a type variable is not allowed to be applied to some type.++mkTypeExpressionT :: HsType -> EnvErrorOr S.TypeExpression+mkTypeExpressionT (HsTyVar var)     = liftM S.TypeVar +                                            (lift (mkTypeVariable var))+mkTypeExpressionT (HsTyApp ty1 ty2) = lift (mkAppTyEx ty1 [ty2])+mkTypeExpressionT (HsTyCon qname)   = lift (mkTypeConstructorApp qname [])++mkTypeExpressionT (HsTyInfix ty1 qname ty2) = -- infix type constructor+  mkTypeExpressionT (HsTyApp (HsTyApp (HsTyCon qname) ty1) ty2)++mkTypeExpressionT (HsTyFun ty1 ty2) = do+  t1 <- mkTypeExpressionT ty1+  t2 <- mkTypeExpressionT ty2+  return (S.TypeFun t1 t2)++mkTypeExpressionT (HsTyTuple Boxed tys)   = do+  ts <- mapM mkTypeExpressionT tys+  return (S.TypeCon (S.ConTuple (length ts)) ts)++mkTypeExpressionT (HsTyForall maybeVars ctx ty) =+  mkForallTyEx (fromMaybe [] maybeVars) ctx ty++mkTypeExpressionT (HsTyPred _) = +  throwError (pp "Implicit parameters are not allowed.")++mkTypeExpressionT (HsTyTuple Unboxed _ ) = +  throwError (pp "Unboxed tuples are not allowed.")++++-- | Checks type abstractions for unique variables, merges the contexts and+--   creates a type expression.++mkForallTyEx :: [HsName] -> HsContext -> HsType -> EnvErrorOr S.TypeExpression+mkForallTyEx vars ctx ty = do+  vs <- unique vars+  cx <- lift (mkContext ctx)+  let unboundVars = (nub . snd . unzip $ cx) \\ vs+  let allVars = vs ++ unboundVars+  knownVars <- ask+  let errVars = knownVars `intersect` unboundVars+  when (not (null errVars)) $ throwError $ pp $ +    "The constrained type variable `" ++ (S.unpackIdent . (\(S.TV i) -> i) . head $ errVars)+    ++ "' must be explicitly quantified."+  liftM (merge allVars cx) (local (++ allVars) (mkTypeExpressionT ty))+  where+    -- Checks if the elements of the argument are unique, and throws an error+    -- otherwise.+    unique :: [HsName] -> EnvErrorOr [S.TypeVariable]+    unique []     = return []+    unique (v:vs) = if v `elem` vs+                      then throwError (pp $+                             "Conflicting type variables in a type "+                             ++ "abstraction, the type variable `"+                             ++ hsNameToString v ++ "' is quantified more "+                             ++ "than once.")+                      else liftM2 (:) (lift (mkTypeVariable v)) (unique vs)++    -- Merges the context and the type expression. The context is represented+    -- as type abstractions.+    merge :: +        [S.TypeVariable] -> [(S.TypeClass, S.TypeVariable)] +        -> S.TypeExpression -> S.TypeExpression+    merge vs cx t = foldr (\v -> S.TypeAbs v (classes cx v)) t vs++    -- Returns classes constraining v.+    classes cx v = nub (map fst (filter ((==) v . snd) cx))++++-- | Collects applied types and transforms them into a type expression.++mkAppTyEx :: HsType -> [HsType] -> ErrorOr S.TypeExpression+mkAppTyEx ty tys = case ty of+  HsTyFun _ _   -> throwError $ pp ("A function type must not be applied to a "+                                    ++ "type.")+  HsTyTuple _ _ -> throwError (pp "A tuple type must not be applied to a type.")+  HsTyVar _     -> throwError (pp "A variable must not be applied to a type.")+  HsTyApp t1 t2 -> mkAppTyEx t1 (t2 : tys)+  HsTyCon qname -> mapM mkTypeExpression tys >>= mkTypeConstructorApp qname ++++-- | Interprets a qualified name as a type constructor and applies it to a list+--   of type expressions.+--   The function type constructor is handled specially because it has to have+--   exactly two arguments.++mkTypeConstructorApp :: +    HsQName +    -> [S.TypeExpression] +    -> ErrorOr S.TypeExpression++mkTypeConstructorApp (Special HsFunCon) [t1,t2] = return $ S.TypeFun t1 t2+mkTypeConstructorApp (Special HsFunCon) _       = throwError errorTypeConstructorApp++mkTypeConstructorApp qname              ts      = +  liftM (\con -> S.TypeCon con ts) (mkTypeConstructor qname)++errorTypeConstructorApp =+  pp "The function type constructor `->' must be applied to exactly two types."++++-- | Transforms a qualified name into a type constructor.+--   Special care is taken for primitive types which could be qualified by+--   \'Prelude\'.++mkTypeConstructor :: HsQName -> ErrorOr S.TypeConstructor+mkTypeConstructor (Qual (Module mod) hsName) = +  if mod == "Prelude"+    then return (asCon hsName)+    else return (S.Con $ hsNameToIdentifier hsName)+mkTypeConstructor (UnQual hsName)          = return $ asCon hsName+mkTypeConstructor (Special HsUnitCon)      = return $ S.ConUnit+mkTypeConstructor (Special HsListCon)      = return $ S.ConList+mkTypeConstructor (Special (HsTupleCon n)) = return $ S.ConTuple n++-- missing case '(Special HsFunCon)' cannot occur,+-- see function 'mkTypeCOnstructorApp'++-- missing case '(Special HsCons)' cannot occur,+-- this is not valid Haskell syntax++++-- | Transforms a name into a type constructor. This functions differentiates+--   between primitive types and other types.++asCon :: HsName -> S.TypeConstructor+asCon name = case name of+  HsIdent "Int"     -> S.ConInt+  HsIdent "Integer" -> S.ConInteger+  HsIdent "Float"   -> S.ConFloat+  HsIdent "Double"  -> S.ConDouble+  HsIdent "Char"    -> S.ConChar+  otherwise         -> S.Con $ hsNameToIdentifier name++++-- | Transforms a Haskell name into a type variable.++mkTypeVariable :: HsName -> ErrorOr S.TypeVariable+mkTypeVariable = return . S.TV . hsNameToIdentifier++++-- | Transforms a qualified Haskell name into an identifier.+--   The module part of a qualified name is ignored.+--   This function fails with an appropriate error message when applied to a+--   special Haskell constructor, i.e. a unit, list, function or tuple+--   constructor.++mkIdentifierQ :: HsQName -> ErrorOr S.Identifier+mkIdentifierQ (UnQual hsName)          = return (hsNameToIdentifier hsName)+mkIdentifierQ (Qual (Module _) hsName) = return (hsNameToIdentifier hsName)++mkIdentifierQ (Special HsUnitCon)      = throwErrorIdentifierQ "`()'"+mkIdentifierQ (Special HsListCon)      = throwErrorIdentifierQ "`[]'"+mkIdentifierQ (Special HsFunCon)       = throwErrorIdentifierQ "`->'"+mkIdentifierQ (Special HsCons)         = throwErrorIdentifierQ "`:'"+mkIdentifierQ (Special (HsTupleCon _)) = throwErrorIdentifierQ "for tuples"++throwErrorIdentifierQ s = throwError $ pp $+  "The constructor " ++ s ++ " must not be used as an identifier."++++-- | Transforms a Haskell name into an identifier.+--   This function encapsulates 'hsNameToIdentifier' into the 'ErrorOr' monad.++mkIdentifier :: HsName -> ErrorOr S.Identifier+mkIdentifier = return . hsNameToIdentifier++++-- | Transforms a Haskell name into an identifier.++hsNameToIdentifier :: HsName -> S.Identifier+hsNameToIdentifier = S.Ident . hsNameToString++++-- | Transforms a Haskell name into a string.+--   Haskell symbols are surrounded by parentheses.++hsNameToString :: HsName -> String+hsNameToString (HsIdent s)  = s+hsNameToString (HsSymbol s) = "(" ++ s ++ ")"+++

@@ -0,0 +1,58 @@++++module Language.Haskell.FreeTheorems.PrettyBase where++++import Text.PrettyPrint++++-- | Prints a list of documents where all documents not fitting on a line are+--   printed in following lines indented by the amount given as the first+--   argument.++isep :: Int -> [Doc] -> Doc+isep _ [] = empty+isep n (d:ds) = nest n $ fsep $ (nest (-n) d) : ds++++-- | Puts parentheses around a document, if the first argument is 'True'.++parensIf :: Bool -> Doc -> Doc+parensIf putParens = if putParens then parens else id++++-- | A data type to describe around which type expressions parentheses are to be+--   put.++data Parens+  = NoParens        -- ^ Don't put any parentheses.+  | ParensFun       -- ^ The type expression occurs as an argument to a+                    --   function.+  | ParensFunOrCon  -- ^ The type expression occurs as an argument to a+                    --   function, type constructor or type class.+  deriving (Eq, Ord)++++-- | Returns a document when a condition holds. Otherwise, the empty document+--   is returned.++when :: Bool -> Doc -> Doc+when False = const empty+when True  = id++++-- | Returns a list of documents when a condition holds. Otherwise, the empty+--   list is returned.++whenL :: Bool -> [Doc] -> [Doc]+whenL False = const []+whenL True  = id++

@@ -0,0 +1,464 @@++++-- | Pretty printer for theorems.+--   It provides functions to transform theorems into documents.+--+--   See the module \"Text.PrettyPrint\" for more details about the used+--   document type.++module Language.Haskell.FreeTheorems.PrettyTheorems (+    PrettyTheoremOption (..)+  , prettyTheorem+  , prettyRelationVariable+  , prettyUnfoldedLift+  , prettyUnfoldedClass+) where++++import Data.List (partition, find)+import Data.Maybe (mapMaybe)+import Text.PrettyPrint++import Language.Haskell.FreeTheorems.Syntax+import Language.Haskell.FreeTheorems.LanguageSubsets+import Language.Haskell.FreeTheorems.Theorems+import Language.Haskell.FreeTheorems.PrettyBase+import Language.Haskell.FreeTheorems.PrettyTypes++++------- Options ---------------------------------------------------------------+++-- | Possible options for pretty-printing theorems.++data PrettyTheoremOption+  = OmitTypeInstantiations      +        -- ^ Omits all instantiations of types. This option makes theorems +        --   usually better readable.+  +  | OmitLanguageSubsets+        -- ^ Omit mentioning language subsets explicitly for certain relations.+  +  deriving Eq++++------- Pretty control data ---------------------------------------------------+++data PrettyControl = PrettyControl+  { options     :: [PrettyTheoremOption]+  , parentheses :: Parens+  , inPremise   :: Bool+  }+++defaultPrettyControl :: [PrettyTheoremOption] -> PrettyControl+defaultPrettyControl opts = +  PrettyControl+    { options = opts+    , parentheses = NoParens+    , inPremise = False+    }+++withTypeInstantiations :: PrettyControl -> Bool+withTypeInstantiations = notElem OmitTypeInstantiations . options+++withLanguageSubsets :: PrettyControl -> Bool+withLanguageSubsets = notElem OmitLanguageSubsets . options+++noParens :: PrettyControl -> PrettyControl+noParens pc = pc { parentheses = NoParens }+++useParens :: PrettyControl -> PrettyControl+useParens pc = pc { parentheses = ParensFun }+++withParens :: PrettyControl -> Bool+withParens pc = parentheses pc > NoParens+++setPremise :: PrettyControl -> PrettyControl+setPremise pc = pc { inPremise = not (inPremise pc) }++++++------- Language subsets ------------------------------------------------------+++-- | Pretty-prints a language subset.++prettyLanguageSubset :: LanguageSubset -> Doc+prettyLanguageSubset l = case l of+  BasicSubset                       -> text "basic"+  SubsetWithFix EquationalTheorem   -> text "fix" <> comma <> text "="+  SubsetWithFix InequationalTheorem -> text "fix" <> comma <> text "[="+  SubsetWithSeq EquationalTheorem   -> text "seq" <> comma <> text "="+  SubsetWithSeq InequationalTheorem -> text "seq" <> comma <> text "[="++++++------- Formulas --------------------------------------------------------------+++-- | Pretty-prints a theorem.++prettyTheorem :: [PrettyTheoremOption] -> Theorem -> Doc+prettyTheorem opt = prettyFormula (defaultPrettyControl opt)++++-- | Pretty-prints a formula.++prettyFormula :: PrettyControl -> Formula -> Doc+prettyFormula pc (ForallRelations v (t1,t2) res f) =+  let rv = prettyRelationVariable v+      ts = prettyTypeExpression NoParens t1 <> comma +           <> prettyTypeExpression NoParens t2+      cs = getTypeClasses res+      ds = if null cs+             then empty+             else parens . fsep . punctuate comma . map prettyTypeClass $ cs+   in parensIf (withParens pc) $ +        sep +          [ fsep $+              [ text "forall"+              , ts, text "in", text "TYPES" <> ds <> comma+              , rv, text "in"+              , text "REL" <> parens ts+                 <> if null res then char '.' else comma ]+              ++ prettyRestrictionList rv res+          , nest 1 (prettyFormula (noParens pc) f) ]++prettyFormula pc (ForallFunctions v (t1,t2) res f) =+  let ts = prettyTypeExpression NoParens t1 <> comma +           <> prettyTypeExpression NoParens t2+      pv = either prettyTermVariable prettyTermVariable v+      cs = getTypeClasses res+      ds = if null cs+             then empty+             else parens . fsep . punctuate comma . map prettyTypeClass $ cs+   in parensIf (withParens pc) $ +        sep +          [ fsep $+              [ text "forall"+              , ts, text "in", text "TYPES" <> ds <> comma +              , pv, text "::"+              , prettyTypeExpression NoParens +                (either (\_ -> TypeFun t1 t2) (\_ -> TypeFun t2 t1) v)+                 <> if null res then char '.' else comma ]+              ++ prettyRestrictionList pv res+          , nest 1 (prettyFormula (noParens pc) f) ]++prettyFormula pc (ForallPairs (v1,v2) r f) =+  parensIf (withParens pc) $+    sep [ fsep [ text "forall"+               , parens (prettyTermVariable v1 <> comma +                         <+> prettyTermVariable v2)+               , text "in", prettyRelation (useParens pc) False r <> char '.' ]+        , nest 1 (prettyFormula (noParens pc) f) ]++prettyFormula pc (ForallVariables v t f) =+  parensIf (withParens pc) $+    sep [ fsep [ text "forall", prettyTermVariable v, text "::"+               , prettyTypeExpression NoParens t <> char '.' ]+        , nest 1 (prettyFormula (noParens pc) f) ]++prettyFormula pc (Equivalence f1 f2) =+  parensIf (withParens pc) $+    sep [ prettyFormula (useParens pc) f1+        , text "<=>" <+> prettyFormula (useParens pc) f2]++prettyFormula pc (Implication f1 f2) =+  parensIf (withParens pc) $+    sep [ prettyFormula (useParens (setPremise pc)) f1+        , text "==>" <+> prettyFormula (useParens pc) f2]++prettyFormula pc (Conjunction f1 f2) =+  parensIf (withParens pc) $+    sep [ prettyFormula (useParens pc) f1+        , text "&&" <+> prettyFormula (useParens pc) f2]++prettyFormula pc (Predicate predicate) = +  parensIf (withParens pc) (prettyPredicate (noParens pc) predicate)++++-- | Returns the type classes of a restriction list.++getTypeClasses :: [Restriction] -> [TypeClass]+getTypeClasses = concatMap exTC+  where exTC r = case r of+          RespectsClasses tcs -> tcs+          otherwise           -> []++++-- | Pretty-prints a list of restrictions.++prettyRestrictionList :: Doc -> [Restriction] -> [Doc]+prettyRestrictionList v res = case res of+  []         -> []+  (r:[])     -> v : [ prettyRestriction r <> char '.' ]+  (r1:r2:[]) -> v : (punctuate comma [prettyRestriction r1] ++ [text "and", prettyRestriction r2 <> char '.' ])+  otherwise  -> let dres = map prettyRestriction res+                 in v : (punctuate comma (init dres ++ [text "and"]) +                        ++ [last dres <> char '.' ])++++-- | Pretty-prints a restriction.++prettyRestriction :: Restriction -> Doc+prettyRestriction Strict           = text "strict"+prettyRestriction Continuous       = text "continuous"+prettyRestriction Total            = text "total"+prettyRestriction BottomReflecting = text "bottom-reflecting"+prettyRestriction LeftClosed       = text "left-closed"+prettyRestriction (RespectsClasses tcs) =+  when (not (null tcs)) $+    fsep [ text "respects"+         , parensIf (length tcs > 1) $+             fsep . punctuate comma . map prettyTypeClass $ tcs ]++++-- | Pretty-prints a predicate.++prettyPredicate :: PrettyControl -> Predicate -> Doc+prettyPredicate pc (IsMember x y r) =+  fsep [ parens (prettyTerm (noParens pc) x <> comma +                 <+> prettyTerm (noParens pc) y)+       , text "in", prettyRelation (useParens pc) False r ]++prettyPredicate pc (IsEqual x y) = +  fsep [ prettyTerm (noParens pc) x, char '=', prettyTerm (noParens pc) y ]++prettyPredicate pc (IsLessEq x y) = +  fsep [ prettyTerm (noParens pc) x, text "[=", prettyTerm (noParens pc) y ]++prettyPredicate pc (IsNotBot x) = +  parensIf (withParens pc) $+    fsep [ prettyTerm (noParens pc) x, text "/=", text "_|_" ]++++-- | Pretty-prints a term.++prettyTerm :: PrettyControl -> Term -> Doc+prettyTerm pc (TermVar v) = prettyTermVariable v++prettyTerm pc (TermApp t1 t2) = +  parensIf (withParens pc) $ prettyTerm (noParens pc) t1 <+> prettyTerm (useParens pc) t2++prettyTerm pc (TermIns t ty) =+  let d = prettyTypeExpression NoParens ty+      withTypes = withTypeInstantiations pc+      p = if withTypes then useParens else noParens+      pt = prettyTerm (useParens pc) t +   in pt <> showInstantiation withTypes d++++-- | Shows an instantiation (by a type).++showInstantiation :: Bool -> Doc -> Doc+showInstantiation False _ = empty+showInstantiation True  d = char '_' <> braces d+++-- | Pretty-prints a term variable.++prettyTermVariable :: TermVariable -> Doc+prettyTermVariable (TVar v) = text v++++------- Relations -------------------------------------------------------------+++-- | Pretty-prints a relation.++prettyRelation :: PrettyControl -> Bool -> Relation -> Doc+prettyRelation _ _ (RelVar _ rv) = prettyRelationVariable rv++prettyRelation pc _ (FunVar ri (Left t)) = +  case theoremType (relationLanguageSubset ri) of +    EquationalTheorem   -> prettyTerm (noParens pc) t+    InequationalTheorem -> prettyTerm (useParens pc) t <> text " ; [="++prettyRelation pc _ (FunVar _ (Right t)) = +  text "[= ; " <> prettyTerm (useParens pc) t <> text "^{-1}"++prettyRelation _ _ (RelBasic ri) = +  case theoremType (relationLanguageSubset ri) of+    EquationalTheorem   -> text "id"+    InequationalTheorem -> text "[="++prettyRelation pc omitOrder (RelLift ri con rs) =+  let pl = case relationLanguageSubset ri of+             BasicSubset -> text "lift"+             otherwise   -> case theoremType (relationLanguageSubset ri) of+                              EquationalTheorem   -> text "lift"+                              InequationalTheorem -> if omitOrder+                                                       then text "lift"+                                                       else text "[= ; lift"+   in pl <> braces (prettyTypeConstructor con)+         <> (parens . foldl1 (\a b -> a <> comma <> b)  +                    . map (prettyRelation (noParens pc) False) $ rs)+--         <> (parens . fsep . punctuate comma +--                           . map (prettyRelation (noParens pc) False) $ rs)+++prettyRelation pc _ (RelFun ri r1 r2) = +  let l = if withLanguageSubsets pc+            then case relationLanguageSubset ri of+                   SubsetWithSeq _ -> text "^" <> braces (prettyLanguageSubset +                                                  (relationLanguageSubset ri))+                   otherwise       -> empty+            else empty+   in parensIf (withParens pc) $+        fsep [ prettyRelation (useParens pc) False r1+             , text "->" <> l+             , prettyRelation (useParens pc) False r2 ]++prettyRelation pc _ (RelAbs ri v _ res r) = +  let tcs = getTypeClasses res+      dcs = if null tcs+              then empty+              else parens (fcat . punctuate comma . map prettyTypeClass $ tcs)+   in parensIf (withParens pc) $+        fsep [ text "forall"+             , prettyRelationVariable v+             , text "in"+             , text "REL" +                <> (when (withLanguageSubsets pc) $+                     text "^" <> braces (prettyLanguageSubset +                                          (relationLanguageSubset ri)))+                <> dcs+                <> char '.'+             , prettyRelation (useParens pc) False r ]++prettyRelation pc _ (FunAbs ri v _ res r) =+  let tcs = getTypeClasses res+      dcs = if null tcs+              then empty+              else parens (fcat . punctuate comma . map prettyTypeClass $ tcs)+   in parensIf (withParens pc) $+        fsep [ text "forall"+             , either prettyTermVariable prettyTermVariable v+             , text "in"+             , either (const (text "FUN")) (const (text "FUN_i")) v+                <> (when (withLanguageSubsets pc) $+                     text "^" <> braces (prettyLanguageSubset +                                          (relationLanguageSubset ri)))+                <> dcs+                <> char '.'+             , prettyRelation (useParens pc) False r ]++++++-- | Pretty-prints a relation variable.++prettyRelationVariable :: RelationVariable -> Doc+prettyRelationVariable (RVar r) = text r++++++------- Unfolded formulas -----------------------------------------------------+++-- | Pretty-prints an unfolded lift relation.++prettyUnfoldedLift :: [PrettyTheoremOption] -> UnfoldedLift -> Doc+prettyUnfoldedLift opt (UnfoldedLift r dcs) =+  let pc = defaultPrettyControl opt+      sc = braces . fsep . punctuate comma . map (prettyUnfoldedDataCon pc) +           $ simpleCons+      ccs = map (braces . prettyUnfoldedDataCon pc) complexCons+      dcs = if null simpleCons then ccs else sc : ccs+   in vcat $+        [ prettyRelation (noParens pc) True r ]+        ++ zipWith (\t d -> nest 2 (text t <+> d)) ("=" : repeat "u") dcs+  where+    (simpleCons, complexCons) = partition isSimpleCon dcs++    isSimpleCon d = case d of+      BotPair   -> True+      ConPair _ -> True+      otherwise -> False++++-- | Pretty-prints an unfolded data constructor declaration.++prettyUnfoldedDataCon :: PrettyControl -> UnfoldedDataCon -> Doc+prettyUnfoldedDataCon _ BotPair = +  parens (fsep (punctuate comma [ text "_|_", text "_|_" ]))++prettyUnfoldedDataCon _ (ConPair d) =+  let d' = prettyDataConstructor d []+   in parens (fsep (punctuate comma [ d', d' ]))++prettyUnfoldedDataCon pc (ConMore d xs ys f) = +  let d1 = prettyDataConstructor d xs+      d2 = prettyDataConstructor d ys+   in sep [ fsep [ parens . fsep . punctuate comma $ [d1, d2] +                 , text "|" ]+          , nest 2 (prettyFormula pc f) ]++++-- | Pretty-prints a data constructor.++prettyDataConstructor :: DataConstructor -> [TermVariable] -> Doc+prettyDataConstructor DConEmptyList _    = brackets empty+prettyDataConstructor DConConsList [x,y] = fsep [prettyTermVariable x, text ":"+                                                , prettyTermVariable y]+prettyDataConstructor DConConsList _     = brackets empty+prettyDataConstructor (DConTuple _) xs = +  parens (fsep . punctuate comma . map prettyTermVariable $ xs)+prettyDataConstructor (DCon s) xs = fsep (text s : map prettyTermVariable xs)++++-- | Pretty-prints an unfolded type class.++prettyUnfoldedClass :: [PrettyTheoremOption] -> UnfoldedClass -> Doc+prettyUnfoldedClass opt (UnfoldedClass tcs tc v fs) =+  let pc = defaultPrettyControl opt+      pv = either prettyRelationVariable prettyTermVariable v +      intro = [ pv, text "respects", prettyTypeClass tc ] +   in if null tcs && null fs+        then fsep $ intro ++ (map text . words $+                      "without further restrictions")+        else vcat $+               (fsep $+                  intro ++ [text "if"]+                  ++ if null tcs+                       then []+                       else [ pv, text "respects" ]+                            ++ (punctuate comma . map prettyTypeClass $ tcs)+                  ++ if not (null tcs) && not (null fs)+                       then [ text "and" ]+                       else [])+               : (map (nest 2 . prettyFormula pc) fs)++++

@@ -0,0 +1,285 @@++++-- | Pretty printer for Haskell declarations.+--   It provides functions to transform declarations and especially type+--   signatures into documents.+--+--   See the module \"Text.PrettyPrint\" for more details about the used+--   document type.++module Language.Haskell.FreeTheorems.PrettyTypes where++++import Text.PrettyPrint++import Language.Haskell.FreeTheorems.BasicSyntax+import Language.Haskell.FreeTheorems.PrettyBase++++------- Declarations ----------------------------------------------------------+++-- | Pretty-prints a declaration.++prettyDeclaration :: Declaration -> Doc+prettyDeclaration (TypeDecl decl)    = prettyTypeDeclaration decl+prettyDeclaration (DataDecl decl)    = prettyDataDeclaration decl+prettyDeclaration (NewtypeDecl decl) = prettyNewtypeDeclaration decl+prettyDeclaration (ClassDecl decl)   = prettyClassDeclaration decl+prettyDeclaration (TypeSig decl)     = prettySignature decl+++instance Show Declaration where+  show = show . prettyDeclaration+  showList ds = (++) (show . vcat . map prettyDeclaration $ ds)++++-- | Pretty-prints a type declaration.++prettyTypeDeclaration :: TypeDeclaration -> Doc+prettyTypeDeclaration (Type ident vs t) =+  isep 2 (+    [text "type", prettyIdentifier ident]+    ++ map prettyTypeVariable vs+    ++ [text "=", prettyTypeExpression NoParens t])++instance Show TypeDeclaration where+  show = show . prettyTypeDeclaration++++-- | Pretty-prints a data declaration.++prettyDataDeclaration :: DataDeclaration -> Doc+prettyDataDeclaration (Data ident vs ds) = +  isep 4 [ isep 2 (+             [text "data", prettyIdentifier ident]+             ++ (map prettyTypeVariable vs))+         , vcat (zipWith (<+>) (char '=' : repeat (char '|'))+                               (map prettyDataConstructorDeclaration ds))]++instance Show DataDeclaration where+  show = show . prettyDataDeclaration++++-- | Pretty-prints a data constructor declaration.++prettyDataConstructorDeclaration :: DataConstructorDeclaration -> Doc+prettyDataConstructorDeclaration (DataCon ident bs) = +  isep 2 $ [prettyIdentifier ident] ++ map prettyBangTypeExpression bs++instance Show DataConstructorDeclaration where+  show = show . prettyDataConstructorDeclaration++++-- | Pretty-prints a type expression having an optional strictness flag.++prettyBangTypeExpression :: BangTypeExpression -> Doc+prettyBangTypeExpression (Banged t)   = char '!'+                                        <> prettyTypeExpression ParensFunOrCon t+prettyBangTypeExpression (Unbanged t) = prettyTypeExpression ParensFunOrCon t++instance Show BangTypeExpression where+  show = show . prettyBangTypeExpression++++-- | Pretty-prints a newtype declaration.++prettyNewtypeDeclaration :: NewtypeDeclaration -> Doc+prettyNewtypeDeclaration (Newtype ident vs con t) =+  isep 2 (+    [text "newtype", prettyIdentifier ident]+    ++ map prettyTypeVariable vs+    ++ [char '=', prettyIdentifier con, prettyTypeExpression ParensFunOrCon t])++instance Show NewtypeDeclaration where+  show = show . prettyNewtypeDeclaration++++-- | Pretty-prints a class declaration.++prettyClassDeclaration :: ClassDeclaration -> Doc+prettyClassDeclaration (Class scs ident tv sigs) =+  let ctx = zip scs (repeat tv)+   in isep 2 [text "class", prettyContext ctx, prettyIdentifier ident,+              prettyTypeVariable tv,+              if null sigs then empty else text "where"]+      $$ nest 4 (vcat (map prettySignature sigs))++instance Show ClassDeclaration where+  show = show . prettyClassDeclaration++++-- | Pretty-prints a type signature.++prettySignature :: Signature -> Doc+prettySignature (Signature ident t) =+  isep 2 [prettyIdentifier ident, text "::", prettyTypeExpression NoParens t]++instance Show Signature where+  show = show . prettySignature++++-- | Pretty-prints a class context constraining certain type variables.++prettyContext :: [(TypeClass, TypeVariable)] -> Doc+prettyContext []  = empty+prettyContext ctx =+  let prettyCV (c,v) = prettyTypeClass c <+> prettyTypeVariable v+   in fsep (+        (parensIf ((length ctx) > 1) +                  (fsep $ punctuate comma $ map prettyCV ctx))+        : [text "=>"])++++------- Type expressions ------------------------------------------------------+++instance Show TypeExpression where+  showsPrec d t = +    let p = case d of+              0         -> NoParens+              1         -> ParensFun+              otherwise -> ParensFunOrCon+     in (++) (show (prettyTypeExpression p t))++++-- | Pretty-prints a type expression.++prettyTypeExpression :: Parens -> TypeExpression -> Doc++prettyTypeExpression _ (TypeVar v) = prettyTypeVariable v++prettyTypeExpression _ (TypeCon ConUnit _) = prettyTypeConstructor ConUnit++prettyTypeExpression _ (TypeCon ConList [t]) =+  brackets (prettyTypeExpression NoParens t)++    -- the following two cases are given to pretty-print also invalid+    -- type expressions, they should usually not occur+prettyTypeExpression _ (TypeCon ConList []) = prettyTypeConstructor ConList+prettyTypeExpression _ (TypeCon ConList (_:_:_)) = brackets (text "...")++prettyTypeExpression _ (TypeCon (ConTuple _) ts) = +  parens $ fsep $ punctuate comma $ map (prettyTypeExpression NoParens) ts++prettyTypeExpression _ (TypeCon ConInt _)     = prettyTypeConstructor ConInt+prettyTypeExpression _ (TypeCon ConInteger _) = prettyTypeConstructor ConInteger+prettyTypeExpression _ (TypeCon ConFloat _)   = prettyTypeConstructor ConFloat+prettyTypeExpression _ (TypeCon ConDouble _)  = prettyTypeConstructor ConDouble+prettyTypeExpression _ (TypeCon ConChar _)    = prettyTypeConstructor ConChar++prettyTypeExpression p (TypeCon (Con ident) ts) =+  parensIf (p >= ParensFunOrCon && not (null ts)) $+    isep 2 $ (prettyIdentifier ident) +             : (map (prettyTypeExpression ParensFunOrCon) ts)++prettyTypeExpression p (TypeFun t1 t2) =+  parensIf (p > NoParens) $ +    fsep (zipWith (<+>) (empty : repeat (text "->")) +                        (map (prettyTypeExpression ParensFun) (t1 : funs t2)))+  where+    funs (TypeFun t1 t2) = t1 : funs t2+    funs t               = [t]++prettyTypeExpression p (TypeAbs v tcs t) =+  let (vs, cx, t') = collectAbstractions v tcs t+   in parensIf (p > NoParens) $+        fsep $ +          [text "forall"] ++ (map prettyTypeVariable vs)+          ++ [char '.', prettyContext cx, prettyTypeExpression NoParens t']++prettyTypeExpression p (TypeExp te) = prettyFixedTypeExpression te++++-- | Collects all type abstractions which follow each other. This is used to get+--   a more compact output.++collectAbstractions :: +    TypeVariable +    -> [TypeClass] +    -> TypeExpression +    -> ([TypeVariable], [(TypeClass, TypeVariable)], TypeExpression)++collectAbstractions v tcs t =+  let cx = zip tcs (repeat v)+   in case t of+        TypeAbs v' tcs' t' -> +          let (vs, cx', t'') = collectAbstractions v' tcs' t'+           in (v : vs, cx ++ cx', t'')+         +        otherwise          -> ([v], cx, t)++++-- | Pretty-prints a type constructor.++prettyTypeConstructor :: TypeConstructor -> Doc+prettyTypeConstructor ConUnit      = parens (empty)  +prettyTypeConstructor ConList      = brackets (empty)+prettyTypeConstructor (ConTuple n) =+  parens . hcat . punctuate comma . take n . repeat $ empty+prettyTypeConstructor ConInt       = text "Int"+prettyTypeConstructor ConInteger   = text "Integer"+prettyTypeConstructor ConFloat     = text "Float"+prettyTypeConstructor ConDouble    = text "Double"+prettyTypeConstructor ConChar      = text "Char"+prettyTypeConstructor (Con c)      = prettyIdentifier c ++++-- | Pretty-prints a type variable.++prettyTypeVariable :: TypeVariable -> Doc+prettyTypeVariable (TV ident) = prettyIdentifier ident++instance Show TypeVariable where+  show = show . prettyTypeVariable++++-- | Pretty-prints a type class.++prettyTypeClass :: TypeClass -> Doc+prettyTypeClass (TC ident) = prettyIdentifier ident++instance Show TypeClass where+  show = show . prettyTypeClass++++-- | Pretty-prints a fixed type expression.++prettyFixedTypeExpression :: FixedTypeExpression -> Doc+prettyFixedTypeExpression (TF ident) = prettyIdentifier ident++instance Show FixedTypeExpression where+  show = show . prettyFixedTypeExpression++++-- | Pretty-prints an identifier.++prettyIdentifier :: Identifier -> Doc+prettyIdentifier (Ident i) = text i++instance Show Identifier where+  show = show . prettyIdentifier+++++

@@ -0,0 +1,54 @@++++-- | Declars data types describing the abstract syntax of a subset of Haskell+--   in the FreeTheorems library. Only declarations and type expressions are+--   covered by these data types.+--+--   Note that the data types of this module do not reflect Haskell98.+--   This is because they are able to express higher-rank functions which are+--   not part of Haskell98.+--   Also, in type expressions, a type variable must not be applied to any type+--   expression. Thus, for example, the type @m a@, as occuring in the functions+--   of the @Monad@ type class, is not expressable.+--   The reason for this restriction is that the FreeTheorems library cannot+--   handle such types.++module Language.Haskell.FreeTheorems.Syntax (++    -- * Declarations++    Declaration (..)+  , getDeclarationName+  , getDeclarationArity+  , DataDeclaration (..)+  , NewtypeDeclaration (..)+  , TypeDeclaration (..)+  , ClassDeclaration (..)+  , Signature (..)+  , DataConstructorDeclaration (..)+  , BangTypeExpression (..)+  ++    -- * Type expressions++  , TypeExpression (..)+  , TypeConstructor (..)+  , TypeClass (..)+  , TypeVariable (..)+  , FixedTypeExpression (..)+++    -- * Identifiers++  , Identifier (..)++) where++++import Language.Haskell.FreeTheorems.BasicSyntax+import Language.Haskell.FreeTheorems.ValidSyntax+import Language.Haskell.FreeTheorems.PrettyTypes++

@@ -0,0 +1,230 @@++++-- | Data structures to describe theorems generated from types.++module Language.Haskell.FreeTheorems.Theorems where++++import Data.Generics (Typeable, Data)++import Language.Haskell.FreeTheorems.BasicSyntax+import Language.Haskell.FreeTheorems.LanguageSubsets++++-- | A theorem which is generated from a type signature.++type Theorem = Formula++++-- | Logical formula constituting automatically generated theorems.++data Formula +  = ForallRelations RelationVariable (TypeExpression, TypeExpression)+                    [Restriction] Formula+        -- ^ Quantifies a relation variable and two type expressions.+  +  | ForallFunctions (Either TermVariable TermVariable) +                    (TypeExpression, TypeExpression) [Restriction] Formula+        -- ^ Quantifies a function variable and two type expressions.+  +  | ForallPairs (TermVariable, TermVariable) Relation Formula+        -- ^ Quantifies two term variables taken from a relation.+  +  | ForallVariables TermVariable TypeExpression Formula+        -- ^ Quantifies a term variable of a certain type.+  +  | Equivalence Formula Formula+        -- ^ Two formulas are equivalent.+  +  | Implication Formula Formula+        -- ^ The first formula implies the second formula.+  +  | Conjunction Formula Formula+        -- ^ The first formula and the second formula.+  +  | Predicate Predicate+        -- ^ A basic formula.+  +  deriving (Typeable, Data)++++-- | Restrictions on functions and relations.++data Restriction+  = Strict+  | Continuous+  | Total+  | BottomReflecting+  | LeftClosed+  | RespectsClasses [TypeClass]+  deriving (Typeable, Data, Eq)++++-- | Predicates occurring in formulas.++data Predicate+  = IsMember Term Term Relation+        -- ^ The pair of two terms is contained in a relation.+  +  | IsEqual Term Term+        -- ^ Two terms are equal.+  +  | IsLessEq Term Term+        -- ^ The first term is less defined than the second one, based on the+        --   semantical approximation order.+  +  | IsNotBot Term+        -- ^ The term is not equal to @_|_@.+  +  deriving (Typeable, Data)++++-- | Terms consisting of variables, applications and instantiations.++data Term+  = TermVar TermVariable            -- ^ A term variable.+  | TermIns Term TypeExpression     -- ^ Instantiation of a term.+  | TermApp Term Term               -- ^ Application of a term to a term.+  deriving (Typeable, Data, Eq)++++-- | Variables occurring in terms.++newtype TermVariable = TVar String+  deriving (Typeable, Data, Eq)++++-- | Relations are the foundations of free theorems.++data Relation+  = RelVar RelationInfo RelationVariable +        -- ^ A relation variable.+ +  | FunVar RelationInfo (Either Term Term)+        -- ^ A function variable.+        --   It might be either a function to be applied on the left side (in+        --   equational and inequational cases) or on the right side (in +        --   inequational cases only).+        --   In inequational cases, the term is additionally composed with the+        --   semantic approximation partial order.+ +  | RelBasic RelationInfo+        -- ^ A basic relation corresponding to a nullary type constructor.+        --   Depending on the theorem type, this can be either an equivalence+        --   relation or the semantic approximation partial order.+  +  | RelLift RelationInfo TypeConstructor [Relation]+        -- ^ A lifted relation for any nonnullary type constructor.+        --   The semantics of lifted relations is differs with the language+        --   subset:+        --   In inequational subsets lifted relations explicitly require+        --   left-closedness by composition with the semantic approximation +        --   partial order.+        --   In equational subsets with fix or seq, this relation requires+        --   strictness explicitly by relating the undefined value with itself.+  +  | RelFun RelationInfo Relation Relation+        -- ^ A relation corresponding to a function type constructor.+        --   The semantics of this relation differs with the language subset:+        --   In the equational subset with seq, this relation is explicitly+        --   requiring bottom-reflectiveness of its members.+        --   In the inequational subset with seq, this relation is explicitly+        --   requiring totality of its members.+  +  | RelAbs RelationInfo RelationVariable (TypeExpression, TypeExpression)+           [Restriction] Relation+        -- ^ A relation corresponding to a type abstraction.++  | FunAbs RelationInfo (Either TermVariable TermVariable)+           (TypeExpression, TypeExpression) [Restriction] Relation+        -- ^ A quantified function.++  deriving (Typeable, Data, Eq)++++-- | Extracts the relation information from a relation.++relationInfo :: Relation -> RelationInfo+relationInfo rel = case rel of+  RelVar ri _       -> ri+  FunVar ri _       -> ri+  RelBasic ri       -> ri+  RelLift ri _ _    -> ri+  RelFun ri _ _     -> ri+  RelAbs ri _ _ _ _ -> ri+  FunAbs ri _ _ _ _ -> ri++++-- | The relation information stored with every relation.++data RelationInfo = RelationInfo+  { relationLanguageSubset :: LanguageSubset+        -- ^ The language subset in which a relation was generated.+  +  , relationLeftType       :: TypeExpression+        -- ^ The type of the first components of pairs contained in a relation.+  +  , relationRightType      :: TypeExpression+        -- ^ The type of the second components of pairs contained in a +        --   relation.+  +  }+  deriving (Typeable, Data, Eq)++++-- | A relation variable.++newtype RelationVariable = RVar String+  deriving (Typeable, Data, Eq)++++-- | Describes unfolded lift relations.++data UnfoldedLift = UnfoldedLift Relation [UnfoldedDataCon]+  deriving (Typeable, Data)++++-- | A relational descriptions of a data constructor.++data UnfoldedDataCon+  = BotPair+  | ConPair DataConstructor+  | ConMore DataConstructor [TermVariable] [TermVariable] Formula+  deriving (Typeable, Data)++++-- | Data constructors.++data DataConstructor+  = DConEmptyList   -- ^ The nullary data constructor @[]@.+  | DConConsList    -- ^ The binary data constructor @:@.+  | DConTuple Int   -- ^ The n-ary tuple data constructor.+  | DCon String     -- ^ Any other data constructor.+  deriving (Typeable, Data)++++-- | A relational description of a class declaration.++data UnfoldedClass +  = UnfoldedClass [TypeClass] TypeClass (Either RelationVariable TermVariable)+                  [Formula]+  deriving (Typeable, Data)+++

@@ -0,0 +1,521 @@++++module Language.Haskell.FreeTheorems.Unfold (+    asTheorem+  , unfoldFormula+  , unfoldLifts+  , unfoldClasses+) where++++import Control.Monad (liftM)+import Control.Monad.State (StateT, get, put, evalStateT, evalState)+import Control.Monad.Reader (Reader, ask, local, runReader, runReaderT)+import Data.Generics (everything, extQ, listify, Data, mkQ)+import Data.List (unfoldr, nub, find, (\\), nubBy)+import Data.Map as Map (fromList)+import Data.Maybe (fromJust)++import Language.Haskell.FreeTheorems.BasicSyntax+import Language.Haskell.FreeTheorems.ValidSyntax+import Language.Haskell.FreeTheorems.LanguageSubsets+import Language.Haskell.FreeTheorems.Intermediate+import Language.Haskell.FreeTheorems.Theorems+import Language.Haskell.FreeTheorems.NameStores++++++------- Basic structures and functions ----------------------------------------+++-- | Abbreviation for the state used to unfold relations to theorems.++type Unfolded a = StateT UnfoldedState (Reader (Bool,Bool)) a++++-- | The state used to unfold relations to theorems.++data UnfoldedState = UnfoldedState +  { newVariableNames :: [String]+        -- ^ An infinite list storing names for variables.+        --   Every element of this list is distinct to the elements of+        --   'newFunctionNames1' and 'newFunctionNames2'.+  +  , newFunctionNames1 :: [String]+        -- ^ An infinite list storing names for functions.+        --   Every element of this list is distinct to the elements of+        --   'newVariableNames' and 'newFunctionNames2'.++  , newFunctionNames2 :: [String]+        -- ^ Another infinite list storing names for functions.+        --   Every element of this list is distinct to the elements of+        --   'newVariableNames' and 'newFunctionNames1'.+  }+  +++-- | Create the initial name store which serves for creating new variable names.++initialState :: Intermediate -> UnfoldedState+initialState ir = +  let fs = intermediateName ir : signatureNames ir+   in UnfoldedState+        { newVariableNames = filter (`notElem` fs) variableNameStore+          -- variable names must not equal the name of the intermediate+          -- variable names don't ever collide with function names or names of+          -- fixed type expressions (see 'NameStores' module)+  +        , newFunctionNames1 = functionVariableNames1 ir+          -- take the name store of functions which was already used during+          -- generation and modification of the intermediate relations++        , newFunctionNames2 = functionVariableNames2 ir+          -- take the name store of functions which was already used during+          -- generation and modification of the intermediate relations+        }+        +++-- | Creates a new term variable. The name is chosen depending on the given+--   type expression, i.e. either a function variable name or a variable name+--   is returned.++newVariableFor :: TypeExpression -> Unfolded TermVariable+newVariableFor t = do+  case t of+    TypeFun _ _    -> do state <- get+                         let ([f], fs) = splitAt 1 (newFunctionNames2 state)+                         put (state { newFunctionNames2 = fs })+                         return (TVar f)+    +    TypeAbs _ _ t' -> newVariableFor t'+    +    otherwise      -> do state <- get+                         let ([x], xs) = splitAt 1 (newVariableNames state)+                         put (state { newVariableNames = xs })+                         return (TVar x)++++-- | Checks if simplifications are possible.++simplificationsAllowed :: Unfolded Bool+simplificationsAllowed = do+  (simplificationPossible, allowAnySimplification) <- ask+  if allowAnySimplification+    then return simplificationPossible+    else return False+++++-- | Toggles the simplification state in the unfolding of the argument.++toggleSimplifications :: Unfolded a -> Unfolded a+toggleSimplifications = local (\(p,a) -> (not p, a))++++++------- Unfolding formulas ----------------------------------------------------+++-- | Unfolds an intermediate structure to a theorem.++asTheorem :: Intermediate -> Theorem+asTheorem i = +  let v = TermVar . TVar . intermediateName $ i+      r = intermediateRelation i+      s = initialState i+   in runReader (evalStateT (unfoldFormula v v r) s) (True, True)++++-- | Unfolds the logical relation "R" in the expression "(x,y) in R" to a+--   theorem. It works by recursively applying unfolding operations of+--   relational actions.++unfoldFormula :: Term -> Term -> Relation -> Unfolded Formula+unfoldFormula x y rel = case rel of+  RelVar _ _           -> return . Predicate . IsMember x y $ rel+  FunVar ri term       -> unfoldTerm x y ri term+  RelBasic ri          -> unfoldBasic x y ri+  RelLift _ _ _        -> return . Predicate . IsMember x y $ rel+  RelFun ri r1 r2      -> unfoldFun x y ri r1 r2+  RelAbs ri v ts res r -> unfoldAbsRel x y ri v ts res r+  FunAbs ri v ts res r -> unfoldAbsFun x y ri v ts res r++++-- | Unfolding operation for terms, i.e. relations specialised to functions.++unfoldTerm :: +    Term -> Term -> RelationInfo -> Either Term Term -> Unfolded Formula+unfoldTerm x y ri term = return . Predicate $+  case term of+    Left t  -> case theoremType (relationLanguageSubset ri) of+                 EquationalTheorem   -> IsEqual (TermApp t x) y+                 InequationalTheorem -> IsLessEq (TermApp t x) y+    Right t -> IsLessEq x (TermApp t y)++++-- | Unfolding operation for nullary relational actions.++unfoldBasic :: Term -> Term -> RelationInfo -> Unfolded Formula+unfoldBasic x y ri = return . Predicate $+  case theoremType (relationLanguageSubset ri) of+    EquationalTheorem   -> IsEqual  x y+    InequationalTheorem -> IsLessEq x y+  +++-- | Unfolding operation for relational actions of type abstractions.++unfoldAbsRel :: +    Term -> Term -> RelationInfo +    -> RelationVariable -> (TypeExpression, TypeExpression)+    -> [Restriction] -> Relation -> Unfolded Formula++unfoldAbsRel x y ri v (t1,t2) res rel = do+  rightSide <- unfoldFormula (TermIns x t1) (TermIns y t2) rel+  return (ForallRelations v (t1, t2) res rightSide)++++-- | Unfolding operation for relational actions of type abstractions+--   (for an abstraction of a function).++unfoldAbsFun :: +    Term -> Term -> RelationInfo +    -> Either TermVariable TermVariable -> (TypeExpression, TypeExpression)+    -> [Restriction] -> Relation -> Unfolded Formula++unfoldAbsFun x y ri v (t1,t2) res rel = do+  rightSide <- unfoldFormula (TermIns x t1) (TermIns y t2) rel+  return (ForallFunctions v (t1, t2) res rightSide)++++-- | Unfolding operation for relational actions of function type constructors.++unfoldFun :: +    Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula+unfoldFun x y ri rel1 rel2 =+  case rel1 of+    RelVar _ _          -> unfoldFunPairs x y ri rel1 rel2+    FunVar _ t          -> +      let ta = either (\t -> Left (TermApp t)) (\t -> Right (TermApp t)) t+          one = unfoldFunOneVar x y ri ta rel1 rel2+          two = unfoldFunVars x y ri rel1 rel2+       in case theoremType (relationLanguageSubset ri) of+            EquationalTheorem   -> one+            InequationalTheorem -> do+              simple <- simplificationsAllowed+              if simple then one else two+    RelBasic _          -> +      case theoremType (relationLanguageSubset ri) of+        EquationalTheorem   -> unfoldFunOneVar x y ri (Left id) rel1 rel2+        InequationalTheorem -> unfoldFunVars x y ri rel1 rel2+    RelLift _ _ _       -> unfoldFunPairs x y ri rel1 rel2+    RelFun _ _ _        -> unfoldFunVars x y ri rel1 rel2 +    RelAbs _ _ _ _ _    -> unfoldFunVars x y ri rel1 rel2+    FunAbs _ _ _ _ _    -> unfoldFunVars x y ri rel1 rel2++++unfoldFunOneVar :: +    Term -> Term -> RelationInfo -> Either (Term -> Term) (Term -> Term) +    -> Relation -> Relation -> Unfolded Formula+unfoldFunOneVar x y ri termapp rel1 rel2 = do+  let t = either (const (relationLeftType (relationInfo rel1))) +                 (const (relationRightType (relationInfo rel1)))+                 termapp+  +  x' <- newVariableFor t+  let tx' = TermVar x'++  f <- case termapp of+         Left t  -> unfoldFormula (TermApp x tx') (TermApp y (t tx')) rel2+         Right t -> unfoldFormula (TermApp x (t tx')) (TermApp y tx') rel2++  addRestriction x y (relationLanguageSubset ri) (ForallVariables x' t f)++++unfoldFunPairs :: +    Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula+unfoldFunPairs x y ri rel1 rel2 = do+  x' <- newVariableFor . relationLeftType  . relationInfo $ rel1+  y' <- newVariableFor . relationRightType . relationInfo $ rel1++  f  <- unfoldFormula (TermApp x (TermVar x')) (TermApp y (TermVar y')) rel2+  +  addRestriction x y (relationLanguageSubset ri) (ForallPairs (x', y') rel1 f)+  +++unfoldFunVars :: +    Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula+unfoldFunVars x y ri rel1 rel2 = do+  let t1 = relationLeftType (relationInfo rel1)+  let t2 = relationRightType (relationInfo rel1)++  x' <- newVariableFor t1+  y' <- newVariableFor t2++  l  <- toggleSimplifications (unfoldFormula (TermVar x') (TermVar y') rel1)+  r  <- unfoldFormula (TermApp x (TermVar x')) (TermApp y (TermVar y')) rel2++  let f = ForallVariables x' t1 (ForallVariables y' t2 (Implication l r))+  addRestriction x y (relationLanguageSubset ri) f++++addRestriction :: Term -> Term -> LanguageSubset -> Formula -> Unfolded Formula+addRestriction x y l f = do+  simple <- simplificationsAllowed+  case l of+    SubsetWithSeq EquationalTheorem -> +      if simple+        then return f+        else let botrefl = Equivalence (Predicate (IsNotBot x))+                                       (Predicate (IsNotBot y))+              in return $ Conjunction botrefl f+    SubsetWithSeq InequationalTheorem -> +      if simple+        then return f+        else return $ Conjunction (Implication (Predicate (IsNotBot x)) +                                               (Predicate (IsNotBot y))) f+    otherwise -> return f++++++------- Unfold lifts ----------------------------------------------------------+++-- | Extracts all lift relations and returns their definition.++unfoldLifts :: [ValidDeclaration] -> Intermediate -> [UnfoldedLift]  +unfoldLifts vds i =+  let decls = map rawDeclaration vds+      rs = collectLifts (intermediateRelation i)++      recUnfold done rs = let (us, ms) = unzip (map unfold rs)+                              ns = concat ms \\ (done ++ rs)+                           in if null ns+                                then us+                                else us ++ recUnfold (done ++ rs) ns+      +      unfold r = case r of +                   RelLift ri con rs -> let (u,ms) = unfoldDecl decls ri con rs+                                         in (UnfoldedLift r u, ms)+      +      eqLift (UnfoldedLift r1 _) (UnfoldedLift r2 _) = r1 == r2+   in nubBy eqLift $ recUnfold [] rs++++collectLifts :: Data a => a -> [Relation]+collectLifts = nub . listify isLift+  where+    isLift rel = case rel of+      RelLift _ _ _ -> True+      otherwise     -> False++++unfoldDecl :: +    [Declaration] -> RelationInfo -> TypeConstructor -> [Relation] +    -> ([UnfoldedDataCon], [Relation])+unfoldDecl decls ri con rs = +  let botPair = case relationLanguageSubset ri of+                  BasicSubset -> []+                  otherwise   -> [BotPair]+      vars t n = map (\i -> TVar (t : show i)) [1..n]+   in case con of+        ConList    -> (botPair ++ unfoldList ri (head rs), [])+        ConTuple n -> (botPair ++ [unfoldTuple n rs], [])+        otherwise  -> +          let d = fromJust (find (isDeclOf con) decls)+           in case d of+                DataDecl d'    -> +                  let ucs = map (unfoldCon (dataVars d') rs) (dataCons d')+                   in (botPair ++ ucs, collectLifts ucs)+                NewtypeDecl d' -> +                  let uc = unfoldCon (newtypeVars d') rs +                                     (DataCon (newtypeCon d') +                                              [Unbanged (newtypeRhs d')])+                   in ([uc], collectLifts uc)+  where+    isDeclOf (Con c) d = case d of+      DataDecl _    -> getDeclarationName d == c+      NewtypeDecl _ -> getDeclarationName d == c+      otherwise     -> False++++unfoldList :: RelationInfo -> Relation -> [UnfoldedDataCon]+unfoldList ri rel = +  let x  = TVar "x"+      y  = TVar "y"+      xs = TVar "xs"+      ys = TVar "ys"+      vs = listify (\(_::TermVariable) -> True) rel+      fs = map (\(TVar v) -> v) (x:y:xs:ys:vs) +   in [ ConPair DConEmptyList+      , ConMore DConConsList [x,xs] [y,ys]+            (Conjunction (unfoldFormulaEx fs (TermVar x, TermVar y, rel))+                         (Predicate (IsMember (TermVar xs) (TermVar ys) +                                              (RelLift ri ConList [rel]))))+      ]+++unfoldTuple :: Int -> [Relation] -> UnfoldedDataCon+unfoldTuple n rs = +  let xs = map (\i -> TVar ('x' : show i)) [1..n]+      ys = map (\i -> TVar ('y' : show i)) [1..n]+      vs = listify (\(_::TermVariable) -> True) rs+      fs = map (\(TVar v) -> v) (xs ++ ys ++ vs)+      txs = map TermVar xs+      tys = map TermVar ys+      th = foldl1 Conjunction (map (unfoldFormulaEx fs) (zip3 txs tys rs))+   in ConMore (DConTuple n) xs ys th++++unfoldCon :: +    [TypeVariable] -> [Relation] -> DataConstructorDeclaration +    -> UnfoldedDataCon+unfoldCon vs rs (DataCon name ts) =+  if null ts+    then ConPair (DCon (unpackIdent name))+    else let n  = length ts+             xs = map (\i -> TVar ('x' : show i)) [1..n]+             ys = map (\i -> TVar ('y' : show i)) [1..n]+             is = map (interpretEx ([], []) vs rs . withoutBang) ts+             os = listify (\(_::TermVariable) -> True) rs+             fs = map (\(TVar v) -> v) (xs ++ ys ++ os)+             txs = map TermVar xs+             tys = map TermVar ys+             th = foldl1 Conjunction (map (unfoldFormulaEx fs) +                                          (zip3 txs tys is))+          in ConMore (DCon (unpackIdent name)) xs ys th+                              +++++unfoldFormulaEx :: +    [String] -> (Term, Term, Relation) -> Formula+unfoldFormulaEx forbidden (x, y, rel) = +  let s = UnfoldedState+          { newVariableNames = filter (`notElem` forbidden) variableNameStore+          , newFunctionNames1 = filter (`notElem` forbidden) functionNameStore1+          , newFunctionNames2 = filter (`notElem` forbidden) functionNameStore2+          }+   in runReader (evalStateT (unfoldFormula x y rel) s) (True, False)+                                                    ++interpretEx :: +    ([String], [TypeExpression]) -> [TypeVariable] -> [Relation] +    -> TypeExpression -> Relation+interpretEx ns vs rs t = +  let e = Map.fromList (zip vs rs)+      l = relationLanguageSubset . relationInfo . head $ rs+   in evalState (runReaderT (interpretM l t) e) ns+++++++------- Exported functions ----------------------------------------------------+++-- | Extracts all class constraints and returns their definition.++unfoldClasses :: [ValidDeclaration] -> Intermediate -> [UnfoldedClass]+unfoldClasses vds i = +  let ds = map rawDeclaration vds+      cs = collectClasses (intermediateRelation i)+      ns = map (\(TVar n) -> n) (listify (\(_::TermVariable) -> True) cs)+      fs = signatureNames i ++ [intermediateName i] ++ ns+      rs = interpretNameStore i+      +      recUnfold done cs =+        let (us, os) = unzip (map (unfoldClass rs ds fs) cs)+            done' = done ++ cs +            ns = concat os \\ done'+         in if null ns+              then us+              else us ++ recUnfold done' ns++   in recUnfold [] cs++++collectClasses :: Data a => a -> [(Relation, TypeClass)]+collectClasses = nub . everything (++) ([] `mkQ` getCC)+  where+    getCC rel = case rel of+      RelAbs ri rv (t1,t2) res _ -> +        let cs  = concatMap getClasses res+            ri' = ri { relationLeftType = t1+                     , relationRightType = t2 }+            r   = RelVar ri' rv+         in map (\c -> (r, c)) cs+      FunAbs ri fv (t1, t2) res _ ->+        let cs  = concatMap getClasses res+            ri' = ri { relationLeftType = t1+                     , relationRightType = t2 }+            r   = FunVar ri' (either (Left . TermVar) (Right . TermVar) fv)+         in map (\c -> (r, c)) cs+      otherwise           -> []++    getClasses r = case r of+      RespectsClasses tcs -> tcs+      otherwise           -> []++++unfoldClass :: +    ([String], [TypeExpression]) -> [Declaration] -> [String] +    -> (Relation, TypeClass) -> (UnfoldedClass, [(Relation, TypeClass)])+unfoldClass istore decls forbiddenNames (r, c@(TC name)) =+  let ClassDecl d = fromJust (find (\d -> getDeclarationName d == name) decls)+      ri = relationInfo r++      interpretSig s = interpretEx istore [classVar d] [r] (signatureType s)+      +      methodName = TermVar . TVar . unpackIdent . signatureName+      leftMethod s = TermIns (methodName s) (relationLeftType ri)+      rightMethod s = TermIns (methodName s) (relationRightType ri)+      +      asFormula s = unfoldFormulaEx+                      forbiddenNames +                      (leftMethod s, rightMethod s, interpretSig s)++      fs = map asFormula (classFuns d)++      ps = map (\c -> (r,c)) (superClasses d)+      ds = concatMap collectClasses fs++      v = case r of+            RelVar _ rv -> Left rv+            FunVar _ fv -> either (Right . unterm) (Right . unterm) fv+      unterm (TermVar v) = v+   +   in (UnfoldedClass (superClasses d) c v fs, ps ++ ds)++++

@@ -0,0 +1,52 @@++++-- | Declares data types which describe valid declarations and valid type +--   signatures. A declaration or type signature is valid when all checks (see+--   "Language.Haskell.FreeTheorems.Frontend") were passed successfully.++module Language.Haskell.FreeTheorems.ValidSyntax where++++import Data.Generics (Typeable, Data)+import Data.Maybe (mapMaybe)++import Language.Haskell.FreeTheorems.BasicSyntax++++-- | Marks a valid declaration.++data ValidDeclaration = ValidDeclaration +  { rawDeclaration :: Declaration +        -- ^ Returns the declaration structure hidden in a valid declaration.++  , isStrictDeclaration :: Bool+        -- ^ Indicates whether the declarations declares or depends on an +        --   algebraic data type with strictness flag.+  }++++-- | Marks a valid type signature.++newtype ValidSignature = ValidSignature +  { rawSignature :: Signature+        -- ^ Returns the signature structure hidden in a valid type signature.+  }++++-- | Extracts all type signatures from a list of declarations.++filterSignatures :: [ValidDeclaration] -> [ValidSignature]+filterSignatures = mapMaybe asSignature+  where +    asSignature (ValidDeclaration decl _) = +      case decl of+        TypeSig sig -> Just (ValidSignature sig)+        otherwise   -> Nothing+++

@@ -0,0 +1,100 @@++++module ParserPrettyPrinterTests (tests) where++++import Control.Monad (liftM, replicateM)+import Control.Monad.Writer (runWriter)+import Data.Generics (everywhere, mkT)+import Test.QuickCheck+import Text.PrettyPrint (vcat)++import Language.Haskell.FreeTheorems.Syntax+import qualified Language.Haskell.FreeTheorems.Parser.Haskell98 as Haskell98+import qualified Language.Haskell.FreeTheorems.Parser.Hsx as Hsx+import Language.Haskell.FreeTheorems.PrettyTypes++import Tests++++-- | All test cases.++tests :: IO ()+tests = do+  doTest "Haskell98.parse . prettyPrint == id" prop_parsePrettyPrint_Haskell98+  doTest "Hsx.parse . prettyPrint == id" prop_parsePrettyPrint_Hsx++++-- | Property: Parsing a pretty-printed declaration results in the same+--   declaration. This property is based on the Haskell98 parser.++prop_parsePrettyPrint_Haskell98 decls = +  let (pds, es) = runWriter . Haskell98.parse +                            . show . vcat . map prettyDeclaration $ ds+   in not (null ds) ==> (null es && not (null pds) && pds == ds)+  where+    types = decls :: ListOfDeclarations+    ds = map modifyTypeExpressions (getDeclarations decls)++    -- type expressions have to be modified because arbitrary type expressions+    -- may contain FixedTypeExpressions, explicit type abstractions and +    -- type constructors applied to a wrong number of arguments+    modifyTypeExpressions = everywhere (mkT adjustType)++    adjustType t = case t of+      TypeCon ConUnit _       -> TypeCon ConUnit []+      TypeCon ConList []      -> TypeCon ConList [TypeCon ConUnit []]+      TypeCon ConList (x:_)   -> TypeCon ConList [x]+      TypeCon (ConTuple _) [] -> TypeCon ConUnit []+      TypeCon (ConTuple n) xs -> if length xs == 1+                                   then TypeCon ConList xs+                                   else TypeCon (ConTuple (length xs)) xs+      TypeCon ConInt _        -> TypeCon ConInt []+      TypeCon ConInteger _    -> TypeCon ConInteger []+      TypeCon ConFloat _      -> TypeCon ConFloat []+      TypeCon ConDouble _     -> TypeCon ConDouble []+      TypeCon ConChar _       -> TypeCon ConChar []+      TypeAbs _ _ t'          -> t'+      TypeExp (TF i)          -> TypeVar (TV i)+      otherwise               -> t++++-- | Property: Parsing a pretty-printed declaration results in the same+--   declaration. This property is based on the Hsx parser.++prop_parsePrettyPrint_Hsx decls = +  let (pds, es) = runWriter . Hsx.parse +                            . show . vcat . map prettyDeclaration $ ds+   in not (null ds) ==> (null es && not (null pds) && pds == ds)+  where+    types = decls :: ListOfDeclarations+    ds = map modifyTypeExpressions (getDeclarations decls)++    -- type expressions have to be modified because arbitrary type expressions+    -- may contain FixedTypeExpressions, explicit type abstractions and +    -- type constructors applied to a wrong number of arguments+    modifyTypeExpressions = everywhere (mkT adjustType)++    adjustType t = case t of+      TypeCon ConUnit _       -> TypeCon ConUnit []+      TypeCon ConList []      -> TypeCon ConList [TypeCon ConUnit []]+      TypeCon ConList (x:_)   -> TypeCon ConList [x]+      TypeCon (ConTuple _) [] -> TypeCon ConUnit []+      TypeCon (ConTuple n) xs -> if length xs == 1+                                   then TypeCon ConList xs+                                   else TypeCon (ConTuple (length xs)) xs+      TypeCon ConInt _        -> TypeCon ConInt []+      TypeCon ConInteger _    -> TypeCon ConInteger []+      TypeCon ConFloat _      -> TypeCon ConFloat []+      TypeCon ConDouble _     -> TypeCon ConDouble []+      TypeCon ConChar _       -> TypeCon ConChar []+      TypeAbs _ _ t'          -> t'+      TypeExp (TF i)          -> TypeVar (TV i)+      otherwise               -> t++

@@ -0,0 +1,21 @@++++import FrontendTypeExpressionsTests as FrontendTypeExpressions (tests)+import FrontendCheckLocalTests as FrontendCheckLocal (tests)+import FrontendCheckGlobalTests as FrontendCheckGlobal (tests)+import FrontendOtherTests as FrontendOther (tests)+import ParserPrettyPrinterTests as ParserPrettyPrinter (tests)++++-- | Run all tests defined for the FreeTheorems library.++main = do+  FrontendTypeExpressions.tests+  FrontendCheckLocal.tests+  FrontendCheckGlobal.tests+  FrontendOther.tests+  ParserPrettyPrinter.tests+  +

@@ -0,0 +1,38 @@++++-- | Defines functions which help to define tests.++module Tests (+    module Arbitraries+  , doTest+) where++++import Test.QuickCheck++import Arbitraries++++-- | Runs a test in a standardised way.+--   +--   A test must have a label which should not be longer than 75 characters.+--   Otherwise, it is truncated.++doTest :: (Arbitrary a, Show a, Testable b) => String -> (a -> b) -> IO ()+doTest name prop = do+  putStrLn (fixString 75 name ++ ":")+  putStr "   "+  check (defaultConfig {configMaxTest = 100}) prop   -- quickCheck prop+  where+    fixString :: Int -> String -> String+    fixString len s =+      if length s <= len+        then s+        else take (len - 3) s ++ "..."++++