free-theorems 0.2.1 → 0.3

raw patch · 9 files changed

+184/−6 lines, 9 files

Files

• free-theorems.cabal +2/−1
• src/Language/Haskell/FreeTheorems.hs +10/−0
• src/Language/Haskell/FreeTheorems/BasicSyntax.hs +1/−1
• src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs +1/−1
• src/Language/Haskell/FreeTheorems/LanguageSubsets.hs +1/−1
• src/Language/Haskell/FreeTheorems/PrettyTheorems.hs +13/−0
• src/Language/Haskell/FreeTheorems/Theorems.hs +5/−1
• src/Language/Haskell/FreeTheorems/Theorems/Simplify.hs +150/−0
• src/Language/Haskell/FreeTheorems/Unfold.hs +1/−1

@@ -1,5 +1,5 @@ name:           free-theorems-version:        0.2.1+version:        0.3 license:        PublicDomain license-file:   LICENSE author:         Sascha Boehme@@ -47,6 +47,7 @@     Language.Haskell.FreeTheorems.PrettyBase     Language.Haskell.FreeTheorems.PrettyTypes     Language.Haskell.FreeTheorems.PrettyTheorems+    Language.Haskell.FreeTheorems.Theorems.Simplify hs-source-dirs: src extensions:     Generics, DeriveDataTypeable, Rank2Types, PatternSignatures extra-source-files:

@@ -41,6 +41,8 @@ --   (7) Optional: Extract class constraints to show their definition --       ('unfoldClasses') and pretty-print them ('prettyUnfoldedClass'). --+--   (8) Optional: Further simplify the Formulas ('simplify') or UnfoldedLift+--       ('simplifyUnfoldedLift') by syntactic transformations.  module Language.Haskell.FreeTheorems ( @@ -77,7 +79,14 @@   , unfoldLifts   , unfoldClasses +    -- * Simplifications+    --+    -- | These syntactic transformations are only valid for equational theorems+    --   in the basic subset or the subset with fix, as eta reduction will be tried. +  , simplify+  , simplifyUnfoldedLift+     -- * Pretty printing          -- | The pretty printer is based on the module \"Text.PrettyPrint\" which@@ -104,6 +113,7 @@ import Language.Haskell.FreeTheorems.LanguageSubsets import Language.Haskell.FreeTheorems.Intermediate import Language.Haskell.FreeTheorems.Theorems+import Language.Haskell.FreeTheorems.Theorems.Simplify import Language.Haskell.FreeTheorems.Unfold import Language.Haskell.FreeTheorems.PrettyTypes import Language.Haskell.FreeTheorems.PrettyTheorems

@@ -1,4 +1,4 @@-+{-# LANGUAGE DeriveDataTypeable #-}   -- | Declares the basic syntax of a Haskell98 subset enriched with 

@@ -1,4 +1,4 @@-+{-# LANGUAGE ExistentialQuantification, Rank2Types #-}   -- | Defines standard functions for modifying type expressions or retrieving

@@ -1,4 +1,4 @@-+{-# LANGUAGE DeriveDataTypeable #-}  -- | Declares the available Haskell language subsets and the result types for --   generating free theorems. 

@@ -252,8 +252,11 @@   parensIf (withParens pc) $     fsep [ prettyTerm (noParens pc) x, text "/=", text "_|_" ] +prettyPredicate pc (IsTrue) = +  text "True"  + -- | Pretty-prints a term.  prettyTerm :: PrettyControl -> Term -> Doc@@ -268,6 +271,16 @@       p = if withTypes then useParens else noParens       pt = prettyTerm (useParens pc) t     in pt <> showInstantiation withTypes d++prettyTerm pc (TermComp []) = +  text "id"++prettyTerm pc (TermComp [t]) = +  parensIf (withParens pc) $ prettyTerm (noParens pc) t++prettyTerm pc (TermComp (t:ts)) = +  parensIf (withParens pc) $ prettyTerm (noParens pc) t <+> text "." <+>+                             prettyTerm (noParens pc) (TermComp ts)   

@@ -1,4 +1,4 @@-+{-# LANGUAGE DeriveDataTypeable #-}   -- | Data structures to describe theorems generated from types.@@ -81,6 +81,9 @@      | IsNotBot Term         -- ^ The term is not equal to @_|_@.++  | IsTrue+        -- ^ Constant True Predicate      deriving (Typeable, Data) @@ -92,6 +95,7 @@   = TermVar TermVariable            -- ^ A term variable.   | TermIns Term TypeExpression     -- ^ Instantiation of a term.   | TermApp Term Term               -- ^ Application of a term to a term.+  | TermComp [Term]                 -- ^ Composition of function terms   deriving (Typeable, Data, Eq)  

@@ -0,0 +1,150 @@+{-# OPTIONS_GHC -fglasgow-exts #-}++module Language.Haskell.FreeTheorems.Theorems.Simplify+	( simplify+        , simplifyUnfoldedLift+ 	)+where++import Data.Generics+import Data.Generics.Aliases+import Data.Generics.Schemes+import Data.Generics.Text (gshow)++import Language.Haskell.FreeTheorems.Theorems++simplify :: Formula -> Formula+simplify f = gsimplify f++simplifyUnfoldedLift :: UnfoldedLift -> UnfoldedLift+simplifyUnfoldedLift l = gsimplify l+++-- Generics stuff:++type ScopeInfo = [TermVariable]++gsimplify :: Data d => (d -> d)+gsimplify = everywhereScoped (\s -> id+				    `extT` simplifyTerm+                                    `extT` simplifyPredicate+                                    `extT` simplifyFormula s+			     ) []++everywhereScoped :: (ScopeInfo -> GenericT) -> ScopeInfo -> GenericT+everywhereScoped = everywhereContext gupdateScope++-- Remember variables in scope++gupdateScope :: (ScopeInfo -> GenericQ ScopeInfo)+gupdateScope s = s `mkQ` flip updateScopeFormula s++-- This will remember all variables currently in scope+updateScopeFormula :: Formula -> ScopeInfo -> ScopeInfo+updateScopeFormula (ForallFunctions (Left  tv) _ _ _) = (tv:)+updateScopeFormula (ForallFunctions (Right tv) _ _ _) = (tv:)+updateScopeFormula (ForallVariables tv _ _)           = (tv:)+updateScopeFormula _                                  = id+++-- Simplificatoins++simplifyFormula :: ScopeInfo -> Formula -> Formula++-- Remove unused quantified variables+simplifyFormula	_ (ForallVariables tv _ f) | not (tv `occursIn` f) = f+ +-- ∀v.f v == g v ⇒ f == g+simplifyFormula	_ (ForallVariables tv _ (Predicate (t1 `IsEqual` t2)))+                                           | Just (f1,v1) <- toFunApp t1+                                           , Just (f2,v2) <- toFunApp t2+                                           , v1 == v2+				           , (TermVar tv) == v1+                                           = gsimplify $ Predicate (f1 `IsEqual` f2)+ +-- Find definitions, and apply as far as possible+simplifyFormula s (ForallVariables tv t f) | [def] <- possibleDefs tv f+		  	                   = gsimplify $ -- Will loop if the definition+                                                         -- would not remove itself+					        ForallVariables tv t+                                                (replaceTerm s (TermVar tv) def f)+-- Remove empty Implication+simplifyFormula _ (Implication (Predicate IsTrue) f) +                                           = f++-- Nothing to optimize+simplifyFormula _ f                        = f++simplifyPredicate :: Predicate -> Predicate++-- Remove tautologies+simplifyPredicate (IsEqual t1 t2) | t1 == t2+                                  = IsTrue++{- This is wrong: The variable might be constrained:++-- Eta reduction on both sides of an equality+simplifyPredicate (IsEqual t1 t2) | Just (f1,v1) <- toFunApp t1+                                  , Just (f2,v2) <- toFunApp t2+                                  , v1 == v2+                                  = gsimplify (IsEqual f1 f2) -- run simplification again+-}++-- Nothing to optimize+simplifyPredicate p               = p+++simplifyTerm :: Term -> Term++-- Simplify function concatenations+simplifyTerm (TermComp [f]) = f+simplifyTerm (TermComp (f : (TermComp fs) : r))+                            = gsimplify (TermComp (f:fs ++ r))++-- Nothing to optimize+simplifyTerm t                = t+	++-- Actions++replaceTerm :: ScopeInfo -> Term -> Term -> GenericT+replaceTerm s0 t def = everywhereScoped (\s -> mkT (repl s)) s0+  where repl :: ScopeInfo -> Term -> Term+        repl s term | term == t+                    , null (listify (not . (`elem` s)) def)+                    = def+                    | otherwise+                    = term++-- Inspections++toFunApp :: Term -> Maybe (Term, Term)+toFunApp (TermApp f v) | Just (fs,v') <- toFunApp v+                       = Just (TermComp [f,fs],v')+toFunApp (TermApp f v) = Just (f,v)+toFunApp _             = Nothing++occursIn :: (Typeable a, Data a1, Eq a) => a -> a1 -> Bool+e `occursIn` e' = gAny (==e) e'++possibleDefs :: TermVariable -> GenericQ [Term]+possibleDefs tv a = everything (.) (id `mkQ` test) a []+  where test (t1 `IsEqual` t2) | t1 == (TermVar tv) = (t2:)+                               | t2 == (TermVar tv) = (t1:)+        test _                 =  id++-- Generic functions++gAny :: Typeable b => (b -> Bool) -> GenericQ Bool+gAny p = everything (||) (False `mkQ` p)++-- | Extend version of 'everywhere', which keeps information about the context around+everywhereContext :: (ctx -> GenericQ ctx) -> +	             (ctx -> GenericT) ->+                      ctx ->+		      GenericT+everywhereContext ctxUpdate f ctx d+	= let ctx' = ctxUpdate ctx d+          in f ctx (gmapT (everywhereContext ctxUpdate f ctx') d)++

@@ -1,4 +1,4 @@-+{-# LANGUAGE PatternSignatures #-}   module Language.Haskell.FreeTheorems.Unfold (