diff --git a/changelog b/changelog --- a/changelog +++ b/changelog @@ -1,3 +1,10 @@ +tip-lib 0.2.2 (released 2015-12-15): +* New passes: --bool-op-lift, --uniq-locals +* New output mode: Waldmeister +* Type skolemise conjectures more economoically +* Allow induction in presence of nested quantifiers +* Small bug fixes + tip-lib 0.2.1 (released 2015-11-16): * Make haddock documentation build diff --git a/executable/Main.hs b/executable/Main.hs --- a/executable/Main.hs +++ b/executable/Main.hs @@ -8,6 +8,7 @@ import Tip.Pretty.Why3 as Why3 import Tip.Pretty.Isabelle as Isabelle import Tip.Pretty.Haskell as HS +import Tip.Pretty.Waldmeister as Waldmeister import Tip.Pretty import Tip.CallGraph @@ -20,7 +21,7 @@ import Options.Applicative import Control.Monad -data OutputMode = Haskell HS.Mode | Why3 | SMTLIB Bool | Isabelle | TIP | TFF +data OutputMode = Haskell HS.Mode | Why3 | SMTLIB Bool | Isabelle | TIP | TFF | Waldmeister parseOutputMode :: Parser OutputMode parseOutputMode = @@ -36,6 +37,7 @@ <|> flag' (SMTLIB True) (long "smtlib-ax-fun" <> help "SMTLIB output (axiomatise function declarations)") <|> flag' Isabelle (long "isabelle" <> help "Isabelle output") <|> flag' TFF (long "tff" <> help "TPTP TFF output") + <|> flag' Waldmeister (long "waldmeister" <> help "Waldmeister output") <|> flag TIP TIP (long "tip" <> help "TIP output (default)") optionParser :: Parser ([StandardPass], Maybe String, OutputMode, Maybe FilePath) @@ -92,6 +94,17 @@ , SimplifyGently, AxiomatizeDatadecls ] , "p") + Waldmeister -> + ( Waldmeister.ppTheory . freshPass uniqLocals + , passes ++ + [ TypeSkolemConjecture, Monomorphise False + , LambdaLift, AxiomatizeLambdas, LetLift + , CollapseEqual, RemoveAliases + , Monomorphise False + , AxiomatizeFuncdefs2, AxiomatizeDatadeclsUEQ + , SkolemiseConjecture + ] + , "w") Haskell m -> (HS.ppTheory m, passes, "hs") Why3 -> (Why3.ppTheory, passes ++ [CSEMatchWhy3], "mlw") Isabelle -> (Isabelle.ppTheory, passes, "thy") diff --git a/src/Tip/Pass/Conjecture.hs b/src/Tip/Pass/Conjecture.hs --- a/src/Tip/Pass/Conjecture.hs +++ b/src/Tip/Pass/Conjecture.hs @@ -86,10 +86,11 @@ isProve _ = False ty_skolem1 thy (Formula Prove i tvs form) = do - tvs' <- mapM (refreshNamed "sk_") tvs + tv <- freshNamed "sk" + let tvs' = replicate (length tvs) tv return thy { thy_asserts = Formula Prove i [] (makeTyCons (zip tvs tvs') form):thy_asserts thy, - thy_sorts = [ Sort tv [] | tv <- tvs' ] ++ thy_sorts thy } + thy_sorts = [ Sort tv [] ] ++ thy_sorts thy } makeTyCons tvs = transformTypeInExpr $ \ty -> diff --git a/src/Tip/Pass/Induction.hs b/src/Tip/Pass/Induction.hs --- a/src/Tip/Pass/Induction.hs +++ b/src/Tip/Pass/Induction.hs @@ -1,4 +1,5 @@ {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE CPP #-} module Tip.Pass.Induction where @@ -7,6 +8,8 @@ import Tip.Fresh import Induction.Structural +import Tip.Pretty.SMT as SMT + import Control.Applicative import Data.List (find,partition) @@ -39,8 +42,14 @@ induction :: (Name a,Ord a) => [Int] -> Theory a -> Fresh [Theory a] induction coords thy@Theory{..} = case goal of - Formula Prove i tvs (Quant qi Forall lcls body) - | cs@(_:_) <- [ x | x <- coords, x >= length lcls || x < 0 ] -> error $ "Induction coordinates " ++ show cs ++ " out of bounds!" + Formula Prove i tvs (forallView -> (lcls@(_non:_empty),body)) + | cs@(_:_) <- + [ x | x <- coords, x >= length lcls || x < 0 ] + -> error $ unlines + [ "In theory: " ++ show (SMT.ppTheory thy) + , "Induction coordinates " ++ show cs ++ " out of bounds!" + , "on goal: " ++ show (SMT.ppFormula goal) + ] | otherwise -> do (obligs,_) <- unTagMapM diff --git a/src/Tip/Pass/Lift.hs b/src/Tip/Pass/Lift.hs --- a/src/Tip/Pass/Lift.hs +++ b/src/Tip/Pass/Lift.hs @@ -2,13 +2,14 @@ {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE CPP #-} -module Tip.Pass.Lift (lambdaLift, letLift, axiomatizeLambdas) where +module Tip.Pass.Lift (lambdaLift, letLift, axiomatizeLambdas, boolOpLift) where #include "errors.h" import Tip.Core import Tip.Fresh import Tip.Utils +import Data.Char (toLower) import Data.Either import Data.List import Data.Generics.Geniplate @@ -96,6 +97,7 @@ in Just (abs,fm) _ -> Nothing + -- | Axiomatize lambdas. -- -- > f x = \ y -> E[x,y] @@ -161,4 +163,30 @@ mkTyVarName :: Int -> String mkTyVarName x = vars !! x where vars = ["a","b","c","d"] ++ ["t" ++ show i | i <- [0..]] + + +boolOpTop :: Name a => TopLift a +boolOpTop e0 = + case e0 of + Builtin x :@: es | x `elem` [And,Or,Implies] -> + do f <- lift (freshNamed (map toLower (show x))) + as <- lift (sequence [ (`Local` boolType) <$> fresh | _ <- es ]) + let fn = Function f [] as boolType (Builtin x :@: map Lcl as) + tell [fn] + return (applyFunction fn [] es) + _ -> return e0 + + +-- | Lifts boolean operators to the top level +-- +-- replaces +-- (and r s t) +-- with +-- f r s t +-- and +-- f x y z = and x y z +-- +-- Run CollapseEqual and BoolOpToIf afterwards +boolOpLift :: Name a => Theory a -> Fresh (Theory a) +boolOpLift = liftTheory boolOpTop diff --git a/src/Tip/Pass/Monomorphise.hs b/src/Tip/Pass/Monomorphise.hs --- a/src/Tip/Pass/Monomorphise.hs +++ b/src/Tip/Pass/Monomorphise.hs @@ -24,6 +24,7 @@ import Data.Generics.Geniplate import Data.List (union) +import Data.Maybe (catMaybes) import Debug.Trace @@ -102,7 +103,8 @@ ] ++ [ Con TyArr (map trType (args ++ [res])) | args :=>: res :: Type a <- universeBi t - ] + ] ++ + [ Var x | TyVar x :: Type a <- universeBi t ] exprRecords :: forall a . Ord a => Tip.Expr a -> [Expr (Con a) a] exprRecords e = usort $ exprGlobalRecords e ++ exprTypeRecords e @@ -227,8 +229,9 @@ ] FuncDecl (Function f tvs args res body) -> - [ Rule (exprGlobalRecords body) (Con (Pred f) (map Var tvs)) - | enthusiastic_function_inst ] ++ + catMaybes + [ safeRule (Rule (exprGlobalRecords body) (Con (Pred f) (map Var tvs))) + | enthusiastic_function_inst ] ++ sigRule f tvs (map lcl_type args) res ++ map (Rule [Con (Pred f) (map Var tvs)]) (exprGlobalRecords body) diff --git a/src/Tip/Pass/UniqLocals.hs b/src/Tip/Pass/UniqLocals.hs new file mode 100644 --- /dev/null +++ b/src/Tip/Pass/UniqLocals.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Tip.Pass.UniqLocals where + +import Tip.Core +import Tip.Scope as Scope +import Tip.Fresh + +import Control.Monad +import Control.Monad.State +import Control.Applicative + +import qualified Data.Traversable as T + +import qualified Data.Map as M +import qualified Data.Set as S + +uniqLocals :: forall a . Name a => Theory a -> Fresh (Theory a) +uniqLocals thy + = fmap declsToTheory + . mapM (flip evalStateT M.empty . T.traverse uq) + . theoryDecls + $ thy + where + nonlocals = M.keys (types scp) ++ M.keys (Scope.globals scp) + scp = scope thy + uq :: a -> StateT (M.Map a a) Fresh a + uq a | a `elem` nonlocals = do return a + | otherwise = do mb <- gets (M.lookup a) + case mb of + Nothing -> do b <- lift (refresh a) + modify (M.insert a b) + return b + Just b -> do return b + diff --git a/src/Tip/Passes.hs b/src/Tip/Passes.hs --- a/src/Tip/Passes.hs +++ b/src/Tip/Passes.hs @@ -24,6 +24,7 @@ , boolOpToIf , theoryBoolOpToIf , removeBuiltinBool + , boolOpLift -- * Match expressions , addMatch @@ -57,6 +58,7 @@ , induction -- * Miscellaneous + , uniqLocals , dropSuffix -- * Building pass pipelines @@ -84,6 +86,7 @@ import Tip.Pass.AxiomatizeDatadecls import Tip.Pass.SelectConjecture import Tip.Pass.DropSuffix +import Tip.Pass.UniqLocals import Tip.Pass.Induction import Tip.Fresh @@ -107,6 +110,7 @@ | IfToBoolOp | BoolOpToIf | RemoveBuiltinBool + | BoolOpLift | AddMatch | CommuteMatch | RemoveMatch @@ -128,6 +132,7 @@ | ProvedConjecture Int | DeleteConjecture Int | DropSuffix String + | UniqLocals | Induction [Int] deriving (Eq,Ord,Show,Read) @@ -147,6 +152,7 @@ IfToBoolOp -> single $ return . ifToBoolOp BoolOpToIf -> single $ return . theoryBoolOpToIf RemoveBuiltinBool -> single $ removeBuiltinBool + BoolOpLift -> single $ boolOpLift AddMatch -> single $ addMatch CommuteMatch -> single $ commuteMatchTheory RemoveMatch -> single $ removeMatch @@ -168,6 +174,7 @@ ProvedConjecture n -> single $ return . provedConjecture n DeleteConjecture n -> single $ return . deleteConjecture n DropSuffix cs -> single $ dropSuffix cs + UniqLocals -> single $ uniqLocals Induction coords -> induction coords where single m thy = do x <- m thy; return [x] parsePass = @@ -198,6 +205,8 @@ help "Replace and/or by if-then-else", unitPass RemoveBuiltinBool $ help "Replace the builtin bool with a datatype", + unitPass BoolOpLift $ + help "Lift boolean operators to the top level", unitPass AddMatch $ help "Transform SMTLIB-style datatype access into pattern matching", unitPass CommuteMatch $ @@ -255,6 +264,8 @@ long "drop-suffix" <> metavar "SUFFIX-CHARS" <> help "Drop the suffix delimited by some character set", + unitPass UniqLocals $ + help "Make all local variables unique", fmap Induction $ option auto $ long "induction" <> diff --git a/src/Tip/Pretty/Waldmeister.hs b/src/Tip/Pretty/Waldmeister.hs new file mode 100644 --- /dev/null +++ b/src/Tip/Pretty/Waldmeister.hs @@ -0,0 +1,83 @@ +{-# LANGUAGE RecordWildCards, OverloadedStrings, PatternGuards, ViewPatterns, ScopedTypeVariables #-} +module Tip.Pretty.Waldmeister where + +import Text.PrettyPrint + +import qualified Tip.Pretty.SMT as SMT + +import Tip.Pretty +import Tip.Types +import Tip.Core +import Tip.Utils.Rename +import Tip.Utils +import Data.Generics.Geniplate +import Data.Maybe +import Data.Char (isAlphaNum,isDigit) +import Data.List (sortBy) +import Data.Ord (comparing) + +import Control.Monad.State +import Control.Monad + +validChar :: Char -> String +validChar x + | isAlphaNum x = [x] + | x `elem` ("~!@$%^&*_-+=<>.?/" :: String) = [x] + | otherwise = "" + +ppTheory :: (Ord a, PrettyVar a) => Theory a -> Doc +ppTheory + (renameWithBlocks keywords + (disambig (concatMap validChar . varStr)) + -> thy@Theory{..}) = + vcat + [ "NAME" <+> "tip" + , "MODE" <+> if null gs then "COMPLETION" else "PROOF" + , "SORTS" $\ vcat (map (ppVar . sort_name) thy_sorts) + , "SIGNATURE" $\ vcat (map ppSig thy_sigs) + , "ORDERING" $\ + vcat + ["KBO", + hsep (punctuate "," [ppVar (sig_name sig) <> "=1" | sig <- thy_sigs]), + hsep (punctuate " >" + (map (ppVar . sig_name) + (reverse + (sortBy (comparing (length . polytype_args . sig_type)) + thy_sigs))))] + , "VARIABLES" $\ + vcat [ ppVar x <+> ":" <+> ppType t + | Local x t :: Local String <- usort (universeBi thy) ] + , "EQUATIONS" $\ vcat (map ppFormula as) + , "CONCLUSION" $\ vcat (map ppFormula gs) + ] + where + (gs,as) = theoryGoals thy + +ppType :: (Ord a, PrettyVar a) => Type a -> Doc +ppType (TyCon t []) = ppVar t +ppType t = error $ "Waldmeister: cannot handle any sophisticated types: " ++ show (SMT.ppType t) + +ppSig :: (Ord a,PrettyVar a) => Signature a -> Doc +ppSig (Signature f (PolyType [] arg_types res_type)) = + hsep $ [ppVar f,":"] ++ map ppType arg_types ++ ["->",ppType res_type] + +ppFormula :: (Ord a, PrettyVar a) => Formula a -> Doc +ppFormula = ppExpr . snd . forallView . fm_body + +ppExpr :: (Ord a, PrettyVar a) => Expr a -> Doc +ppExpr (Builtin Equal :@: [e1,e2]) = hsep [ppExpr e1,"=",ppExpr e2] +ppExpr (hd :@: []) = ppHead hd +ppExpr (hd :@: es) = hcat ([ppHead hd <> "("] ++ punctuate "," (map ppExpr es)) <> ")" +ppExpr (Lcl l) = ppVar (lcl_name l) +ppExpr Quant{} = error "Waldmeister: cannot handle nested quantifiers" +ppExpr Lam{} = error "Waldmeister: defunctionalize" +ppExpr Match{} = error "Waldmeister: axiomatize funcdecls and lift matches" +ppExpr Let{} = error "Waldmeister: lift let declarations" + +ppHead :: (Ord a, PrettyVar a) => Head a -> Doc +ppHead (Gbl (Global g _ _)) = ppVar g +ppHead (Builtin (Lit (Bool b))) = text (show b) +ppHead (Builtin b) = error $ "Waldmeister: cannot handle any builtins! Offending builtin:" ++ show b + +keywords :: [String] +keywords = words "> -> : NAME MODE SORTS SIGNATURE ORDERING LPO KBO VARIABLES EQUATIONS CONCLUSION PROOF COMPLETION" diff --git a/src/Tip/Utils/Specialiser.hs b/src/Tip/Utils/Specialiser.hs --- a/src/Tip/Utils/Specialiser.hs +++ b/src/Tip/Utils/Specialiser.hs @@ -7,7 +7,7 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE CPP #-} module Tip.Utils.Specialiser - (specialise, Rule(..), Expr(..), + (specialise, safeRule, Rule(..), Expr(..), Void, absurd, Closed, subtermRules, subterms, Subst, Inst) where @@ -20,6 +20,7 @@ import Control.Monad import Data.Maybe import Data.Foldable (Foldable) +import qualified Data.Foldable as F import Data.Traversable (Traversable) import Data.Set (Set) @@ -29,6 +30,8 @@ import Text.PrettyPrint +import Debug.Trace + data Expr c a = Var a | Con c [Expr c a] deriving (Eq,Ord,Show,Functor,Foldable,Traversable) @@ -48,13 +51,24 @@ mapRuleOrd :: (c -> c') -> Rule c a -> Rule c' a mapRuleOrd c = bimapRule c id -instance (Pretty c,Pretty a) => Pretty (Expr c a) where +instance (Pretty a,Pretty c) => Pretty (Expr c a) where pp (Var x) = pp x pp (Con k es) = pp k <+> parens (fsep (punctuate "," (map pp es))) -instance (Pretty c,Pretty a) => Pretty (Rule c a) where - pp (Rule ps q) = parens (fsep (punctuate "," (map pp ps))) <+> "=>" $\ pp q +instance (Eq a, Pretty a,Pretty c) => Pretty (Rule c a) where + pp r@(Rule ps q) = parens (fsep (punctuate "," (map pp ps))) <+> "=>" $\ pp q + $\ (if badRule r then " (bad rule!!)" else Text.PrettyPrint.empty) +-- ok : a b c -> b c +-- bad: b c -> a b c +badRule :: Eq a => Rule c a -> Bool +badRule (Rule ps q) = or [ qv `notElem` concatMap F.toList ps | qv <- F.toList q ] + +safeRule :: Eq a => Rule c a -> Maybe (Rule c a) +safeRule r + | badRule r = Nothing + | otherwise = Just r + subtermRules :: Rule c a -> [Rule c a] subtermRules (Rule p q) = map (Rule p) (subterms q) @@ -104,7 +118,14 @@ go :: [Closed c] -> [Closed c] go insts - | null (new_insts \\ insts) = [] + {- + | traceShow ("go" $\ sep ["insts:" $\ pp insts + ,"new_insts:" $\ pp new_insts + ,"new:" $\ pp new + ]) + False = undefined + -} + | null (new_insts \\ insts) = new_insts | otherwise = new_insts `union` go (new_insts `union` insts) where new_insts = usort $ map (snd . snd) new @@ -114,7 +135,7 @@ which cls = usort [ (d,i) | (d,(i,_)) <- step named_rules cls ] -- Return the safe rules, and the scary rules -separate :: (Ord a,Ord c) => [(name,Rule c a)] -> ([name],[name]) +separate :: (Ord c,Ord a) => [(name,Rule c a)] -> ([name],[name]) separate = go [] where go rs ((n,r):xs) @@ -122,7 +143,7 @@ | otherwise = let (a,b) = go rs xs in ( a,n:b) go _ _ = ([],[]) -terminating :: forall a c . (Ord a,Ord c) => [Rule c a] -> Bool +terminating :: forall a c . (Ord c,Ord a) => [Rule c a] -> Bool terminating (map (mapRuleOrd Old) -> rs) = go 10 S.empty (usort (inst rs)) where go :: Int -> Set (Closed (Sk c)) -> [Closed (Sk c)] -> Bool diff --git a/tip-lib.cabal b/tip-lib.cabal --- a/tip-lib.cabal +++ b/tip-lib.cabal @@ -1,5 +1,5 @@ name: tip-lib -version: 0.2.1 +version: 0.2.2 synopsis: tons of inductive problems - support library and tools description: This package provides a tool for processing inductive theorem proving problems in TIP format (see the homepage for details). homepage: http://tip-org.github.io @@ -35,6 +35,7 @@ Tip.Pretty.Isabelle Tip.Pretty.Haskell Tip.Pretty.TFF + Tip.Pretty.Waldmeister Tip.Parser @@ -58,6 +59,7 @@ Tip.Pass.Conjecture Tip.Pass.CSEMatch Tip.Pass.DropSuffix + Tip.Pass.UniqLocals Tip.Pass.EliminateDeadCode Tip.Pass.EqualFunctions Tip.Pass.FillInCases