tip-lib 0.2.1 → 0.2.2
raw patch · 11 files changed
+229/−17 lines, 11 files
Files
- changelog +7/−0
- executable/Main.hs +14/−1
- src/Tip/Pass/Conjecture.hs +3/−2
- src/Tip/Pass/Induction.hs +11/−2
- src/Tip/Pass/Lift.hs +29/−1
- src/Tip/Pass/Monomorphise.hs +6/−3
- src/Tip/Pass/UniqLocals.hs +34/−0
- src/Tip/Passes.hs +11/−0
- src/Tip/Pretty/Waldmeister.hs +83/−0
- src/Tip/Utils/Specialiser.hs +28/−7
- tip-lib.cabal +3/−1
changelog view
@@ -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
executable/Main.hs view
@@ -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")
src/Tip/Pass/Conjecture.hs view
@@ -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 ->
src/Tip/Pass/Induction.hs view
@@ -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
src/Tip/Pass/Lift.hs view
@@ -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
src/Tip/Pass/Monomorphise.hs view
@@ -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)
+ src/Tip/Pass/UniqLocals.hs view
@@ -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+
src/Tip/Passes.hs view
@@ -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" <>
+ src/Tip/Pretty/Waldmeister.hs view
@@ -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"
src/Tip/Utils/Specialiser.hs view
@@ -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
tip-lib.cabal view
@@ -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