diff --git a/free-theorems.cabal b/free-theorems.cabal --- a/free-theorems.cabal +++ b/free-theorems.cabal @@ -1,5 +1,5 @@ name: free-theorems -version: 0.3 +version: 0.3.1 license: PublicDomain license-file: LICENSE author: Sascha Boehme @@ -18,6 +18,7 @@ may be derived in addition to classical equational results. category: Language tested-with: GHC==6.8.2 +cabal-version: >= 1.2.3 build-type: Simple build-depends: base >= 1.0 @@ -32,10 +33,10 @@ 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 +other-modules: Language.Haskell.FreeTheorems.Frontend Language.Haskell.FreeTheorems.Frontend.Error Language.Haskell.FreeTheorems.Frontend.TypeExpressions diff --git a/src/Language/Haskell/FreeTheorems.hs b/src/Language/Haskell/FreeTheorems.hs --- a/src/Language/Haskell/FreeTheorems.hs +++ b/src/Language/Haskell/FreeTheorems.hs @@ -73,6 +73,7 @@ , Intermediate , interpret , asTheorem + , asCompleteTheorem , relationVariables , specialise , specialiseInverse diff --git a/src/Language/Haskell/FreeTheorems/BasicSyntax.hs b/src/Language/Haskell/FreeTheorems/BasicSyntax.hs --- a/src/Language/Haskell/FreeTheorems/BasicSyntax.hs +++ b/src/Language/Haskell/FreeTheorems/BasicSyntax.hs @@ -204,8 +204,18 @@ | TypeFun TypeExpression TypeExpression -- ^ The function type constructor @->@. + | TypeFunLab TypeExpression TypeExpression + -- ^ The function type constructor @->^o@ for the non-bottom-reflecting + -- logical relation for functions in the languagesubset with seq + -- for equational theorems. + | TypeAbs TypeVariable [TypeClass] TypeExpression -- ^ The type abstraction constructor @forall@. + + | TypeAbsLab TypeVariable [TypeClass] TypeExpression + -- ^ The type abstraction constructor @forall^o@, allowing + -- non-bottom-reflecting logical relations for types the type variable + -- is instantiated with in the calculus with seq. | TypeExp FixedTypeExpression -- ^ A variable representing a fixed type expression. diff --git a/src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs b/src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs --- a/src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs +++ b/src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs @@ -43,9 +43,10 @@ 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 + TypeVar v -> Set.insert v s + TypeAbs v _ _ -> Set.insert v s + TypeAbsLab v _ _ -> Set.insert v s + otherwise -> s @@ -55,9 +56,10 @@ 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 + TypeVar v -> Set.insert v s + TypeAbs v _ _ -> Set.delete v s + TypeAbsLab v _ _ -> Set.delete v s + otherwise -> s @@ -76,8 +78,9 @@ -- 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 + TypeAbs v _ _ -> Map.delete v env + TypeAbsLab v _ _ -> Map.delete v env + otherwise -> env -- Replaces a type variable by a type expression, if the type variable is -- contained in the environment. @@ -124,8 +127,9 @@ -- 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 + TypeAbs v _ _ -> if (v == old) then rep else f + TypeAbsLab 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 @@ -133,8 +137,9 @@ -- 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' + TypeVar v -> TypeVar (r v) + TypeAbs v cs t' -> TypeAbs (rep v) cs t' + TypeAbsLab v cs t' -> TypeAbsLab (rep v) cs t' otherwise -> t diff --git a/src/Language/Haskell/FreeTheorems/Intermediate.hs b/src/Language/Haskell/FreeTheorems/Intermediate.hs --- a/src/Language/Haskell/FreeTheorems/Intermediate.hs +++ b/src/Language/Haskell/FreeTheorems/Intermediate.hs @@ -1,6 +1,3 @@ - - - -- | 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 @@ -152,6 +149,12 @@ ri <- mkRelationInfo l t -- create the relation info liftM2 (RelFun ri) (interpretM l t1) (interpretM l t2) + -- create a second relation for function types (used only for language + -- subset with seq and the equational setting + TypeFunLab t1 t2 -> do + ri <- mkRelationInfo l t -- create the relation info + liftM2 (RelFunLab 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 @@ -161,6 +164,16 @@ let res = relRes l ++ (if null cs then [] else [RespectsClasses cs]) return (RelAbs ri rv (t1,t2) res r) + -- create a second relation for type abstractions (used only for language + -- subset with seq and the equational setting + TypeAbsLab 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 = (filter (/= BottomReflecting) (relRes l)) ++ (if null cs then [] else [RespectsClasses cs]) + return (RelAbs ri rv (t1,t2) res r) + where mkRelationInfo l t = do env <- ask @@ -247,6 +260,7 @@ getRVar ok rel = case rel of RelLift _ _ rs -> concatMap (getRVar ok) rs RelFun _ r1 r2 -> getRVar (not ok) r1 ++ getRVar ok r2 + RelFunLab _ 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 -> [] @@ -294,7 +308,11 @@ 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 + let res'' = either (const funResL) (const funResR) fv + -- hack! should be somehow better implemented + -- if BottomReflecting is not present, we had + -- TypeAbsLab quantification in (SubsetWithSeq Equational) + res' = if elem BottomReflecting res then res'' else filter (/= Total) res'' in if rv == r then FunAbs ri fv ts (res' ++ (classConstraints res)) rel' else rel @@ -337,6 +355,10 @@ else rel RelFun ri r1 r2 -> RelFun ri (re (mk' (not ok) ri r1) r1) (re (mk ok ri r2) r2) + -- second logical relation for functions. Only used for the language + -- subset with Seq in the equational setting + RelFunLab ri r1 r2 -> RelFunLab 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 diff --git a/src/Language/Haskell/FreeTheorems/NameStores.hs b/src/Language/Haskell/FreeTheorems/NameStores.hs --- a/src/Language/Haskell/FreeTheorems/NameStores.hs +++ b/src/Language/Haskell/FreeTheorems/NameStores.hs @@ -3,7 +3,14 @@ -- | Provides functions to generate new variable names of different kinds. -module Language.Haskell.FreeTheorems.NameStores where +module Language.Haskell.FreeTheorems.NameStores + ( typeNameStore + , relationNameStore + , typeExpressionNameStore + , functionNameStore1 + , functionNameStore2 + , variableNameStore + ) where diff --git a/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs b/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs --- a/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs +++ b/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs @@ -41,7 +41,7 @@ | OmitLanguageSubsets -- ^ Omit mentioning language subsets explicitly for certain relations. - + deriving Eq @@ -345,6 +345,13 @@ fsep [ prettyRelation (useParens pc) False r1 , text "->" <> l , prettyRelation (useParens pc) False r2 ] + +-- second function relation only used in the equational setting with Seq +prettyRelation pc _ (RelFunLab ri r1 r2) = + parensIf (withParens pc) $ + fsep [ prettyRelation (useParens pc) False r1 + , text "->^o" <> empty + , prettyRelation (useParens pc) False r2 ] prettyRelation pc _ (RelAbs ri v _ res r) = let tcs = getTypeClasses res diff --git a/src/Language/Haskell/FreeTheorems/PrettyTypes.hs b/src/Language/Haskell/FreeTheorems/PrettyTypes.hs --- a/src/Language/Haskell/FreeTheorems/PrettyTypes.hs +++ b/src/Language/Haskell/FreeTheorems/PrettyTypes.hs @@ -194,6 +194,14 @@ funs (TypeFun t1 t2) = t1 : funs t2 funs t = [t] +prettyTypeExpression p (TypeFunLab t1 t2) = + parensIf (p > NoParens) $ + fsep (zipWith (<+>) (empty : repeat (text "->")) + (map (prettyTypeExpression ParensFun) (t1 : funs t2))) + where + funs (TypeFunLab 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) $ @@ -201,6 +209,13 @@ [text "forall"] ++ (map prettyTypeVariable vs) ++ [char '.', prettyContext cx, prettyTypeExpression NoParens t'] +prettyTypeExpression p (TypeAbsLab 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 @@ -217,11 +232,14 @@ collectAbstractions v tcs t = let cx = zip tcs (repeat v) in case t of - TypeAbs v' tcs' t' -> + TypeAbs v' tcs' t' -> let (vs, cx', t'') = collectAbstractions v' tcs' t' in (v : vs, cx ++ cx', t'') + TypeAbsLab v' tcs' t' -> + let (vs, cx', t'') = collectAbstractions v' tcs' t' + in (v : vs, cx ++ cx', t'') - otherwise -> ([v], cx, t) + otherwise -> ([v], cx, t) diff --git a/src/Language/Haskell/FreeTheorems/Theorems.hs b/src/Language/Haskell/FreeTheorems/Theorems.hs --- a/src/Language/Haskell/FreeTheorems/Theorems.hs +++ b/src/Language/Haskell/FreeTheorems/Theorems.hs @@ -143,6 +143,13 @@ -- requiring bottom-reflectiveness of its members. -- In the inequational subset with seq, this relation is explicitly -- requiring totality of its members. + + | RelFunLab RelationInfo Relation Relation + -- ^ A relation corresponding to a function type constructor. + -- The semantics of this relation differs with the language subset: + -- Apart from the equational subset with seq, it is equal to RelFun. + -- In the equational subset with Seq, this relation is _not_ + -- explicitly requiring bottom-reflectiveness of its members. | RelAbs RelationInfo RelationVariable (TypeExpression, TypeExpression) [Restriction] Relation @@ -165,6 +172,7 @@ RelBasic ri -> ri RelLift ri _ _ -> ri RelFun ri _ _ -> ri + RelFunLab ri _ _ -> ri RelAbs ri _ _ _ _ -> ri FunAbs ri _ _ _ _ -> ri diff --git a/src/Language/Haskell/FreeTheorems/Unfold.hs b/src/Language/Haskell/FreeTheorems/Unfold.hs --- a/src/Language/Haskell/FreeTheorems/Unfold.hs +++ b/src/Language/Haskell/FreeTheorems/Unfold.hs @@ -3,6 +3,7 @@ module Language.Haskell.FreeTheorems.Unfold ( asTheorem + , asCompleteTheorem , unfoldFormula , unfoldLifts , unfoldClasses @@ -28,7 +29,6 @@ - ------- Basic structures and functions ---------------------------------------- @@ -92,6 +92,11 @@ let ([f], fs) = splitAt 1 (newFunctionNames2 state) put (state { newFunctionNames2 = fs }) return (TVar f) + + TypeFunLab _ _ -> do state <- get + let ([f], fs) = splitAt 1 (newFunctionNames2 state) + put (state { newFunctionNames2 = fs }) + return (TVar f) TypeAbs _ _ t' -> newVariableFor t' @@ -136,7 +141,16 @@ in runReader (evalStateT (unfoldFormula v v r) s) (True, True) +-- | Unfolds an intermediate structure to a theorem with _all_ restrictions. +asCompleteTheorem :: Intermediate -> Theorem +asCompleteTheorem i = + let v = TermVar . TVar . intermediateName $ i + r = intermediateRelation i + s = initialState i + in runReader (evalStateT (unfoldFormula v v r) s) (True, False) + + -- | 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. @@ -148,6 +162,7 @@ RelBasic ri -> unfoldBasic x y ri RelLift _ _ _ -> return . Predicate . IsMember x y $ rel RelFun ri r1 r2 -> unfoldFun x y ri r1 r2 + RelFunLab ri r1 r2 -> unfoldFunLab 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 @@ -224,12 +239,39 @@ 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 + RelFun _ _ _ -> unfoldFunVars x y ri rel1 rel2 + RelFunLab _ _ _ -> unfoldFunVars x y ri rel1 rel2 + RelAbs _ _ _ r _ -> unfoldFunVars x y ri rel1 rel2 FunAbs _ _ _ _ _ -> unfoldFunVars x y ri rel1 rel2 +-- | Unfolding operation for relational actions of function type constructors. +unfoldFunLab :: + Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula +unfoldFunLab x y ri rel1 rel2 = + case rel1 of + RelVar _ _ -> unfoldFunLabPairs x y ri rel1 rel2 + FunVar _ t -> + let ta = either (\t -> Left (TermApp t)) (\t -> Right (TermApp t)) t + one = unfoldFunLabOneVar x y ri ta rel1 rel2 + two = unfoldFunLabVars 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 -> unfoldFunLabOneVar x y ri (Left id) rel1 rel2 + InequationalTheorem -> unfoldFunLabVars x y ri rel1 rel2 + RelLift _ _ _ -> unfoldFunLabPairs x y ri rel1 rel2 + RelFun _ _ _ -> unfoldFunLabVars x y ri rel1 rel2 + RelFunLab _ _ _ -> unfoldFunLabVars x y ri rel1 rel2 + RelAbs _ _ _ r _ -> unfoldFunLabVars x y ri rel1 rel2 + FunAbs _ _ _ _ _ -> unfoldFunLabVars x y ri rel1 rel2 + + unfoldFunOneVar :: Term -> Term -> RelationInfo -> Either (Term -> Term) (Term -> Term) -> Relation -> Relation -> Unfolded Formula @@ -246,9 +288,27 @@ Right t -> unfoldFormula (TermApp x (t tx')) (TermApp y tx') rel2 addRestriction x y (relationLanguageSubset ri) (ForallVariables x' t f) +-- return (ForallVariables x' t f) +unfoldFunLabOneVar :: + Term -> Term -> RelationInfo -> Either (Term -> Term) (Term -> Term) + -> Relation -> Relation -> Unfolded Formula +unfoldFunLabOneVar 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) + return (ForallVariables x' t f) + + unfoldFunPairs :: Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula unfoldFunPairs x y ri rel1 rel2 = do @@ -258,7 +318,18 @@ f <- unfoldFormula (TermApp x (TermVar x')) (TermApp y (TermVar y')) rel2 addRestriction x y (relationLanguageSubset ri) (ForallPairs (x', y') rel1 f) +-- return (ForallPairs (x', y') rel1 f) + +unfoldFunLabPairs :: + Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula +unfoldFunLabPairs 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) + return (ForallPairs (x', y') rel1 f) unfoldFunVars :: @@ -275,9 +346,25 @@ let f = ForallVariables x' t1 (ForallVariables y' t2 (Implication l r)) addRestriction x y (relationLanguageSubset ri) f +-- return f +unfoldFunLabVars :: + Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula +unfoldFunLabVars 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)) + return f + + addRestriction :: Term -> Term -> LanguageSubset -> Formula -> Unfolded Formula addRestriction x y l f = do simple <- simplificationsAllowed @@ -320,7 +407,7 @@ in (UnfoldedLift r u, ms) eqLift (UnfoldedLift r1 _) (UnfoldedLift r2 _) = r1 == r2 - in nubBy eqLift $ recUnfold [] rs + in nubBy eqLift $ recUnfold [] rs