diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -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. + + diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,4 @@ +#!/usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain diff --git a/free-theorems.cabal b/free-theorems.cabal new file mode 100644 --- /dev/null +++ b/free-theorems.cabal @@ -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 diff --git a/runtests b/runtests new file mode 100644 --- /dev/null +++ b/runtests @@ -0,0 +1,3 @@ +#!/bin/bash + +runhaskell -isrc -fglasgow-exts src/Runtests.hs diff --git a/src/Arbitraries.hs b/src/Arbitraries.hs new file mode 100644 --- /dev/null +++ b/src/Arbitraries.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] + + diff --git a/src/FrontendCheckGlobalTests.hs b/src/FrontendCheckGlobalTests.hs new file mode 100644 --- /dev/null +++ b/src/FrontendCheckGlobalTests.hs @@ -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 + + + diff --git a/src/FrontendCheckLocalTests.hs b/src/FrontendCheckLocalTests.hs new file mode 100644 --- /dev/null +++ b/src/FrontendCheckLocalTests.hs @@ -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)) + + + diff --git a/src/FrontendOtherTests.hs b/src/FrontendOtherTests.hs new file mode 100644 --- /dev/null +++ b/src/FrontendOtherTests.hs @@ -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 + + + + diff --git a/src/FrontendTypeExpressionsTests.hs b/src/FrontendTypeExpressionsTests.hs new file mode 100644 --- /dev/null +++ b/src/FrontendTypeExpressionsTests.hs @@ -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 + + + + diff --git a/src/InterpretationTests.hs b/src/InterpretationTests.hs new file mode 100644 --- /dev/null +++ b/src/InterpretationTests.hs @@ -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 + +-} + + + diff --git a/src/Language/Haskell/FreeTheorems.hs b/src/Language/Haskell/FreeTheorems.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems.hs @@ -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. +-- +-- +-- * /The Impact of seq on Free Theorems-Based Program Transformations/, +-- Patricia Johann and Janis Voigtländer, Fundamenta Informaticae, +-- 2006. +-- +-- +-- 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. + + diff --git a/src/Language/Haskell/FreeTheorems/BasicSyntax.hs b/src/Language/Haskell/FreeTheorems/BasicSyntax.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/BasicSyntax.hs @@ -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) + + + + diff --git a/src/Language/Haskell/FreeTheorems/Frontend.hs b/src/Language/Haskell/FreeTheorems/Frontend.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Frontend.hs @@ -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)) + + + + + diff --git a/src/Language/Haskell/FreeTheorems/Frontend/CheckGlobal.hs b/src/Language/Haskell/FreeTheorems/Frontend/CheckGlobal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Frontend/CheckGlobal.hs @@ -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) + + + diff --git a/src/Language/Haskell/FreeTheorems/Frontend/CheckLocal.hs b/src/Language/Haskell/FreeTheorems/Frontend/CheckLocal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Frontend/CheckLocal.hs @@ -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 + + + + + diff --git a/src/Language/Haskell/FreeTheorems/Frontend/Error.hs b/src/Language/Haskell/FreeTheorems/Frontend/Error.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Frontend/Error.hs @@ -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) + + + + diff --git a/src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs b/src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs @@ -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 + + + + + + diff --git a/src/Language/Haskell/FreeTheorems/Intermediate.hs b/src/Language/Haskell/FreeTheorems/Intermediate.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Intermediate.hs @@ -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 + + + + + + diff --git a/src/Language/Haskell/FreeTheorems/LanguageSubsets.hs b/src/Language/Haskell/FreeTheorems/LanguageSubsets.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/LanguageSubsets.hs @@ -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) + + + diff --git a/src/Language/Haskell/FreeTheorems/NameStores.hs b/src/Language/Haskell/FreeTheorems/NameStores.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/NameStores.hs @@ -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..]) + + + diff --git a/src/Language/Haskell/FreeTheorems/Parser/Haskell98.hs b/src/Language/Haskell/FreeTheorems/Parser/Haskell98.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Parser/Haskell98.hs @@ -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 ++ ")" + + diff --git a/src/Language/Haskell/FreeTheorems/Parser/Hsx.hs b/src/Language/Haskell/FreeTheorems/Parser/Hsx.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Parser/Hsx.hs @@ -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 ++ ")" + + + diff --git a/src/Language/Haskell/FreeTheorems/PrettyBase.hs b/src/Language/Haskell/FreeTheorems/PrettyBase.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/PrettyBase.hs @@ -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 + + diff --git a/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs b/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs @@ -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) + + + + diff --git a/src/Language/Haskell/FreeTheorems/PrettyTypes.hs b/src/Language/Haskell/FreeTheorems/PrettyTypes.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/PrettyTypes.hs @@ -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 + + + + + diff --git a/src/Language/Haskell/FreeTheorems/Syntax.hs b/src/Language/Haskell/FreeTheorems/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Syntax.hs @@ -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 + + diff --git a/src/Language/Haskell/FreeTheorems/Theorems.hs b/src/Language/Haskell/FreeTheorems/Theorems.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Theorems.hs @@ -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) + + + diff --git a/src/Language/Haskell/FreeTheorems/Unfold.hs b/src/Language/Haskell/FreeTheorems/Unfold.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Unfold.hs @@ -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) + + + + diff --git a/src/Language/Haskell/FreeTheorems/ValidSyntax.hs b/src/Language/Haskell/FreeTheorems/ValidSyntax.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/ValidSyntax.hs @@ -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 + + + diff --git a/src/ParserPrettyPrinterTests.hs b/src/ParserPrettyPrinterTests.hs new file mode 100644 --- /dev/null +++ b/src/ParserPrettyPrinterTests.hs @@ -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 + + diff --git a/src/Runtests.hs b/src/Runtests.hs new file mode 100644 --- /dev/null +++ b/src/Runtests.hs @@ -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 + + diff --git a/src/Tests.hs b/src/Tests.hs new file mode 100644 --- /dev/null +++ b/src/Tests.hs @@ -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 ++ "..." + + + +