diff --git a/Jukebox/Clausify.hs b/Jukebox/Clausify.hs new file mode 100644 --- /dev/null +++ b/Jukebox/Clausify.hs @@ -0,0 +1,446 @@ +{-# LANGUAGE TypeOperators, BangPatterns #-} +module Jukebox.Clausify where + +import Jukebox.Form +import qualified Jukebox.Form as Form +import Jukebox.Name +import Data.List( maximumBy, sortBy, partition ) +import Data.Ord +import Control.Monad.Reader +import Control.Monad.State.Strict +import qualified Jukebox.Seq as S +import Jukebox.Seq(Seq) +import qualified Jukebox.NameMap as NameMap +import Jukebox.NameMap(NameMap) +import qualified Jukebox.Map as Map +import qualified Data.HashSet as Set +import qualified Data.ByteString.Char8 as BS +import Jukebox.Utils +import Jukebox.Options +import Control.Applicative + +newtype ClausifyFlags = ClausifyFlags { splitting :: Bool } deriving Show + +clausifyFlags = + inGroup "Clausifier options" $ + ClausifyFlags <$> + bool "split" + ["Split the conjecture into several sub-conjectures.", + "Default: (off)"] + +---------------------------------------------------------------------- +-- clausify + +clausify :: ClausifyFlags -> Problem Form -> CNF +clausify flags inps = close inps (run . clausifyInputs S.Nil S.Nil) + where + clausifyInputs theory obligs [] = + do return (toObligs (S.toList theory) (S.toList obligs)) + + clausifyInputs theory obligs (inp:inps) | kind inp == Axiom = + do cs <- clausForm (tag inp) (what inp) + clausifyInputs (theory `S.append` cs) obligs inps + + clausifyInputs theory obligs (inp:inps) | kind inp `elem` [Conjecture, Question] = + do clausifyObligs theory obligs (tag inp) (split' (what inp)) inps + + clausifyObligs theory obligs s [] inps = + do clausifyInputs theory obligs inps + + clausifyObligs theory obligs s (a:as) inps = + do cs <- clausForm s (nt a) + clausifyObligs theory (obligs `S.append` S.Unit cs) s as inps + + split' a | splitting flags = if null split_a then [true] else split_a + where split_a = split a + split' a = [a] + +split :: Form -> [Form] +split p = + case positive p of + ForAll (Bind xs p) -> + [ ForAll (Bind xs p') | p' <- split p ] + + And ps -> + concatMap split (S.toList ps) + + p `Equiv` q -> + split (nt p \/ q) ++ split (p \/ nt q) + + Or ps -> + snd $ + maximumBy first + [ (siz q, [ Or (S.fromList (q':qs)) | q' <- sq ]) + | (q,qs) <- select (S.toList ps) + , let sq = split q + ] + + _ -> + [p] + where + select [] = [] + select (x:xs) = (x,xs) : [ (y,x:ys) | (y,ys) <- select xs ] + + first (n,x) (m,y) = n `compare` m + + siz (And ps) = S.length ps + siz (ForAll (Bind _ p)) = siz p + siz (_ `Equiv` _) = 2 + siz _ = 0 + +{- + Or ps | S.size ps > 0 && n > 0 -> + [ Or (S.fromList (p':ps')) | p' <- split p ] + where + pns = [(p,siz p) | p <- S.toList ps] + ((p,n),pns') = getMax (head pns) [] (tail pns) + ps' = [ p' | (p',_) <- pns' ] + + getMax pn@(p,n) pns [] = (pn,pns) + getMax pn@(p,n) pns (qm@(q,m):qms) + | m > n = getMax qm (pn:pns) qms + | otherwise = getMax pn (qm:pns) qms +-} + +---------------------------------------------------------------------- +-- core clausification algorithm + +clausForm :: BS.ByteString -> Form -> M [Input Clause] +clausForm s p = + withName s $ + do miniscoped <- miniscope . check . simplify . check $ p + noEquivPs <- removeEquiv . check $ miniscoped + noExistsPs <- mapM removeExists . check $ noEquivPs + noExpensiveOrPs <- fmap concat . mapM removeExpensiveOr . check $ noExistsPs + noForAllPs <- lift . lift . mapM uniqueNames . check $ noExpensiveOrPs + let !cnf_ = S.concatMap cnf . check $ noForAllPs + !simp = simplifyCNF . fmap S.toList . check $ cnf_ + cs = S.toList . fmap clause $ simp + inps = [ Input (BS.append s (BS.pack i)) Axiom c + | (c, i) <- zip cs ("": + [ '_':show i | i <- [1..] ]) ] + return $! force . check $ inps + +---------------------------------------------------------------------- +-- miniscoping +miniscope :: Form -> M Form +miniscope t@Literal{} = return t +miniscope (Not f) = fmap Not (miniscope f) +miniscope (And fs) = fmap And (S.mapM miniscope fs) +miniscope (Or fs) = fmap Or (S.mapM miniscope fs) +miniscope (Equiv f g) = liftM2 Equiv (miniscope f) (miniscope g) +miniscope (ForAll (Bind xs f)) = miniscope f >>= forAll xs +miniscope (Exists (Bind xs f)) = miniscope f >>= forAll xs . nt >>= return . nt + +forAll :: NameMap Variable -> Form -> M Form +forAll xs a | Map.null xs = return a +forAll xs a = + case positive a of + And as -> + fmap And (S.mapM (forAll xs) as) + + ForAll (Bind ys a) + | Map.null m -> return (ForAll (Bind ys a)) + | otherwise -> fmap (forAll' ys) (forAll m a) + where m = xs Map.\\ ys + forAll' vs (ForAll (Bind vs' t)) = ForAll (Bind (vs `Map.union` vs') t) + forAll' vs t = ForAll (Bind vs t) + + Or as -> forAllOr xs [ (a, free a) | a <- S.toList as ] + + _ -> return (ForAll (Bind xs a)) + +forAllOr :: NameMap Variable -> [(Form, NameMap Variable)] -> M Form +forAllOr xs avss = do { y <- yes; forAll xs' (y \/ no) } + where + v = head (NameMap.toList xs) + xs' = NameMap.delete v xs + (bs1,bs2) = partition ((v `NameMap.member`) . snd) avss + no = orl [ b | (b,_) <- bs2 ] + body = orl [ b | (b,_) <- bs1 ] + yes = case bs1 of + [] -> return (orl []) + [(b,_)] -> forAll (NameMap.singleton v) b + _ -> return (ForAll (Bind (NameMap.singleton v) body)) + orl = foldr (\/) false + +---------------------------------------------------------------------- +-- removing equivalences + +-- removeEquiv p -> ps : +-- POST: And ps is equivalent to p (modulo extra symbols) +-- POST: ps has no Equiv and no Not +removeEquiv :: Form -> M [Form] +removeEquiv p = + do (defs,pos,_) <- removeEquivAux False p + return (S.toList (defs `S.append` S.Unit pos)) + +-- removeEquivAux inEquiv p -> (defs,pos,neg) : +-- PRE: inEquiv is True when we are "under" an Equiv +-- POST: defs is a list of definitions, under which +-- pos is equivalent to p and neg is equivalent to nt p +-- (the reason why "neg" and "nt pos" can be different, is +-- because we want to always code an equivalence as +-- a conjunction of two disjunctions, which leads to fewer +-- clauses -- the "neg" part of the result for the case Equiv +-- below makes use of this) +removeEquivAux :: Bool -> Form -> M (Seq Form,Form,Form) +removeEquivAux inEquiv p = + case simple p of + Not p -> + do (defs,pos,neg) <- removeEquivAux inEquiv p + return (defs,neg,pos) + + And ps -> + do dps <- sequence [ removeEquivAux inEquiv p | p <- S.toList ps ] + let (defss,poss,negs) = unzip3 dps + return ( S.concat defss + , And (S.fromList poss) + , Or (S.fromList negs) + ) + + ForAll (Bind xs p) -> + do (defs,pos,neg) <- removeEquivAux inEquiv p + return ( defs + , ForAll (Bind xs pos) + , Exists (Bind xs neg) + ) + + p `Equiv` q -> + do (defsp,posp,negp) <- removeEquivAux True p + (defsq,posq,negq) <- removeEquivAux True q + (defsp',posp',negp') <- makeCopyable inEquiv posp negp + (defsq',posq',negq') <- makeCopyable inEquiv posq negq + return ( S.concat [defsp, defsq, defsp', defsq'] + , (negp' \/ posq') /\ (posp' \/ negq') + , (negp' \/ negq') /\ (posp' \/ posq') + ) + + Literal l -> + do return (S.Nil,Literal l,Literal (neg l)) + +-- makeCopyable turns an argument to an Equiv into something that we are +-- willing to copy. There are two such cases: (1) when the Equiv is +-- not under another Equiv (because we have to copy arguments to an Equiv +-- at least once anyway), (2) if the formula is small. +-- All other formulas will be made small (by means of a definition) +-- before we copy them. +makeCopyable :: Bool -> Form -> Form -> M (Seq Form,Form,Form) +makeCopyable inEquiv pos neg + | isSmall pos || not inEquiv = + -- we skolemize here so that we reuse the skolem function + -- (if we do this after copying, we get several skolemfunctions) + do pos' <- removeExists pos + neg' <- removeExists neg + return (S.Nil,pos',neg') + + | otherwise = + do dp <- literal "equiv" (free pos) + return (S.fromList [Literal (Neg dp) \/ pos, Literal (Pos dp) \/ neg], Literal (Pos dp), Literal (Neg dp)) + where + -- a formula is small if it is already a literal + isSmall (Literal _) = True + isSmall (Not p) = isSmall p + isSmall (ForAll (Bind _ p)) = isSmall p + isSmall (Exists (Bind _ p)) = isSmall p + isSmall _ = False + +---------------------------------------------------------------------- +-- skolemization + +-- removeExists p -> p' +-- PRE: p has no Equiv and no Not +-- POST: p' is equivalent to p (modulo extra symbols) +-- POST: p' has no Equiv, no Exists, and no Not +removeExists :: Form -> M Form +removeExists (And ps) = + do ps <- sequence [ removeExists p | p <- S.toList ps ] + return (And (S.fromList ps)) + +removeExists (Or ps) = + do ps <- sequence [ removeExists p | p <- S.toList ps ] + return (Or (S.fromList ps)) + +removeExists (ForAll (Bind xs p)) = + do p' <- removeExists p + return (ForAll (Bind xs p')) + +removeExists t@(Exists (Bind xs p)) = + -- skolemterms have only variables as arguments, arities are large(r) + do ss <- sequence [ fmap (x |=>) (skolem x (free t)) | x <- NameMap.toList xs ] + removeExists (subst (foldr (|+|) ids ss) p) + {- + -- skolemterms can have other skolemterms as arguments, arities are small(er) + -- disadvantage: skolemterms are very complicated and deep + do p' <- skolemize p + t <- skolem x (S.delete x (free p')) + return (subst (x |=> t) p') + -} + +removeExists lit = + do return lit + +-- TODO: Avoid recomputing "free" at every step, by having +-- skolemize return the set of free variables as well + +-- TODO: Investigate skolemizing top-down instead, find the right +-- optimization + +---------------------------------------------------------------------- +-- make cheap Ors + +removeExpensiveOr :: Form -> M [Form] +removeExpensiveOr p = + do (defs,p',_) <- removeExpensiveOrAux p + return (S.toList (defs `S.append` S.Unit p')) + +-- cost: represents how it expensive it is to clausify a formula +type Cost = (Integer,Integer) -- (#clauses, #literals) + +unitCost :: Cost +unitCost = (1,1) + +andCost :: [Cost] -> Cost +andCost cs = (sum (map fst cs), sum (map snd cs)) + +orCost :: [Cost] -> Cost +orCost [] = (1,0) +orCost [c] = c +orCost ((c1,l1):cs) = (c1 * c2, c1 * l2 + c2 * l1) + where + (c2,l2) = orCost cs + +removeExpensiveOrAux :: Form -> M (Seq Form,Form,Cost) +removeExpensiveOrAux (And ps) = + do dcs <- sequence [ removeExpensiveOrAux p | p <- S.toList ps ] + let (defss,ps,costs) = unzip3 dcs + return (S.concat defss, And (S.fromList ps), andCost costs) + +removeExpensiveOrAux (Or ps) = + do dcs <- sequence [ removeExpensiveOrAux p | p <- S.toList ps ] + let (defss,ps,costs) = unzip3 dcs + (defs2,p,c) <- makeOr (sortBy (comparing snd) (zip ps costs)) + return (S.concat defss `S.append` defs2,p,c) + +removeExpensiveOrAux (ForAll (Bind xs p)) = + do (defs,p',cost) <- removeExpensiveOrAux p + return (fmap (ForAll . Bind xs) defs, ForAll (Bind xs p'), cost) + +removeExpensiveOrAux lit = + do return (S.Nil, lit, unitCost) + +-- input is sorted; small costs first +makeOr :: [(Form,Cost)] -> M (Seq Form,Form,Cost) +makeOr [] = + do return (S.Nil, false, orCost []) + +makeOr [(f,c)] = + do return (S.Nil,f,c) + +makeOr fcs + | null fcs2 = + do return (S.Nil, Or (S.fromList (map fst fcs1)), orCost (map snd fcs1)) + + | otherwise = + do d <- literal "or" (free (map fst fcs2)) + (defs,p,_) <- makeOr ((Literal (Neg d),unitCost):fcs2) + return ( defs `S.snoc` p + , Or (S.fromList (Literal (Pos d) : map fst fcs1)) + , orCost (unitCost : map snd fcs1) + ) + where + (fcs1,fcs2) = split [] fcs + + split fcs1 [] = (fcs1,[]) + split fcs1 (fc@(_,(cc,_)):fcs) | cc <= 1 = split (fc:fcs1) fcs + split fcs1 fcs@((_,(cc,_)):_) | cc <= 2 = (take 2 fcs ++ fcs1, drop 2 fcs) + split fcs1 fcs = (take 1 fcs ++ fcs1, drop 1 fcs) + +---------------------------------------------------------------------- +-- clausification + +-- cnf p = cs +-- PRE: p has no Equiv, no Exists, and no Not, +-- and each variable is only bound once +-- POST: And (map Or cs) is equivalent to p +cnf :: Form -> Seq (Seq Literal) +cnf (ForAll (Bind _ p)) = cnf p +cnf (And ps) = S.concatMap cnf ps +cnf (Or ps) = cross (fmap cnf ps) +cnf (Literal x) = S.Unit (S.Unit x) + +cross :: Seq (Seq (Seq Literal)) -> Seq (Seq Literal) +cross S.Nil = S.Unit S.Nil +cross (S.Unit x) = x +cross (S.Append cs1 cs2) = liftM2 S.append (cross cs1) (cross cs2) + +---------------------------------------------------------------------- +-- simplification of CNF + +simplifyCNF :: Seq [Literal] -> [[Literal]] +simplifyCNF = + -- nub: don't generate multiple copies of identical clauses + nub . S.concatMap (tautElim . unify []) + where -- remove negative variable equalities X != Y by substitution + unify xs [] = xs + unify xs (Neg (Var v :=: t@Var{}):ys) = + unify (subst (v |=> t) xs) (subst (v |=> t) ys) + unify xs (l:ys) = unify (l:xs) ys + -- simplify p | ~p or t = t to true. + tautElim ls + | Set.null (pos `Set.intersection` neg) && not (any tauto ls) + -- reorder the order of the literals in the clause + -- so that more clauses become equal; + -- also, remove duplicate literals from the clause + = S.Unit (map Neg (Set.toList neg) ++ map Pos (Set.toList pos)) + | otherwise = S.Nil + where pos = Set.fromList [ l | Pos l <- ls ] + neg = Set.fromList [ l | Neg l <- ls ] + tauto (Pos (t :=: u)) = t == u + tauto _ = False + +---------------------------------------------------------------------- +-- monad + +type M = ReaderT Tag (StateT Int NameM) + +run :: M a -> NameM a +run x = evalStateT (runReaderT x BS.empty) 0 + +skolemName :: Named a => String -> a -> M Name +skolemName prefix v = do + i <- get + put (i+1) + s <- getName + lift . lift . newName $ prefix ++ show i ++ concat [ "_" ++ t | t <- map BS.unpack [s, baseName v], not (null t) ] + +nextSk :: M Int +nextSk = do + i <- get + put (i+1) + return i + +withName :: Tag -> M a -> M a +withName s m = lift (runReaderT m s) + +getName :: M Tag +getName = ask + +skolem :: Variable -> NameMap Variable -> M Term +skolem (v ::: t) vs = + do n <- skolemName "sK" v + let f = n ::: FunType (map typ args) t + return (f :@: map Var args) + where + args = NameMap.toList vs + +literal :: String -> NameMap Variable -> M Atomic +literal w vs = + do n <- skolemName "sP" w + let p = n ::: FunType (map typ args) O + return (Tru (p :@: map Var args)) + where + args = NameMap.toList vs + +---------------------------------------------------------------------- +-- the end. diff --git a/Jukebox/Form.hs b/Jukebox/Form.hs new file mode 100644 --- /dev/null +++ b/Jukebox/Form.hs @@ -0,0 +1,716 @@ +-- Formulae, inputs, terms and so on. +-- +-- "Show" instances for several of these types are found in TPTP.Print. + +{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, Rank2Types, GADTs, TypeOperators, ScopedTypeVariables, BangPatterns, PatternGuards #-} +module Jukebox.Form where + +import Prelude hiding (sequence, mapM) +import qualified Jukebox.Seq as S +import Jukebox.Seq(Seq) +import Data.Hashable +import qualified Jukebox.Map as Map +import Jukebox.NameMap(NameMap) +import qualified Jukebox.NameMap as NameMap +import Data.Ord +import qualified Data.ByteString.Char8 as BS +import Jukebox.Name +import Control.Monad.State.Strict hiding (sequence, mapM) +import Data.List hiding (nub) +import Jukebox.Utils +import Data.Typeable(Typeable) +import Data.Monoid +import Data.Traversable + +-- Set to True to switch on some sanity checks +debugging :: Bool +debugging = False + +---------------------------------------------------------------------- +-- Types + +data DomainSize = Finite Int | Infinite deriving (Eq, Ord, Show, Typeable) + +data Type = + O + | Type { + tname :: {-# UNPACK #-} !Name, + -- type is monotone when domain size is >= tmonotone + tmonotone :: DomainSize, + -- if there is a model of size >= tsize then there is a model of size tsize + tsize :: DomainSize } deriving Typeable + +data FunType = FunType { args :: [Type], res :: Type } deriving (Eq, Typeable) + +-- Helper function for defining (Eq, Ord, Hashable) instances +typeMaybeName :: Type -> Maybe Name +typeMaybeName O = Nothing +typeMaybeName Type{tname = t} = Just t + +instance Eq Type where + t1 == t2 = typeMaybeName t1 == typeMaybeName t2 + +instance Ord Type where + compare = comparing typeMaybeName + +instance Hashable Type where + hashWithSalt s = hashWithSalt s . typeMaybeName + +instance Named Type where + name O = nameO + name Type{tname = t} = t + +-- Typeclass of "things that have a type" +class Typed a where + typ :: a -> Type + +instance Typed Type where + typ = id + +instance Typed FunType where + typ = res + +instance Typed b => Typed (a ::: b) where + typ (_ ::: t) = typ t + +---------------------------------------------------------------------- +-- Terms + +type Variable = Name ::: Type +type Function = Name ::: FunType +data Term = Var Variable | Function :@: [Term] deriving (Eq, Ord) + +instance Hashable Term where + hashWithSalt s = hashWithSalt s . convert + where convert (Var x) = Left x + convert (f :@: ts) = Right (f, ts) + +instance Named Term where + name (Var x) = name x + name (f :@: _) = name f + +instance Typed Term where + typ (Var x) = typ x + typ (f :@: _) = typ f + +newSymbol :: Named a => a -> b -> NameM (Name ::: b) +newSymbol x ty = fmap (::: ty) (newName x) + +newFunction :: Named a => a -> [Type] -> Type -> NameM Function +newFunction x args res = newSymbol x (FunType args res) + +newType :: Named a => a -> NameM Type +newType x = do + n <- newName x + return (Type n Infinite Infinite) + +funArgs :: Function -> [Type] +funArgs (_ ::: ty) = args ty + +arity :: Function -> Int +arity = length . funArgs + +size :: Term -> Int +size Var{} = 1 +size (f :@: xs) = 1 + sum (map size xs) + +---------------------------------------------------------------------- +-- Literals + +infix 8 :=: +data Atomic = Term :=: Term | Tru Term + +-- Helper for (Eq Atomic, Ord Atomic, Hashable Atomic) instances +normAtomic :: Atomic -> Either (Term, Term) Term +normAtomic (t1 :=: t2) | t1 > t2 = Left (t2, t1) + | otherwise = Left (t1, t2) +normAtomic (Tru p) = Right p + +instance Eq Atomic where + t1 == t2 = normAtomic t1 == normAtomic t2 + +instance Ord Atomic where + compare = comparing normAtomic + +instance Hashable Atomic where + hashWithSalt s = hashWithSalt s . normAtomic + +data Signed a = Pos a | Neg a deriving (Show, Eq, Ord) + +instance Hashable a => Hashable (Signed a) where + hashWithSalt s = hashWithSalt s . convert + where convert (Pos x) = Left x + convert (Neg x) = Right x + +instance Functor Signed where + fmap f (Pos x) = Pos (f x) + fmap f (Neg x) = Neg (f x) +type Literal = Signed Atomic + +neg :: Signed a -> Signed a +neg (Pos x) = Neg x +neg (Neg x) = Pos x + +the :: Signed a -> a +the (Pos x) = x +the (Neg x) = x + +pos :: Signed a -> Bool +pos (Pos _) = True +pos (Neg _) = False + +signForm :: Signed a -> Form -> Form +signForm (Pos _) f = f +signForm (Neg _) f = Not f + +---------------------------------------------------------------------- +-- Formulae + +-- Invariant: each name is bound only once on each path +-- i.e. nested quantification of the same variable twice is not allowed +-- Not OK: ![X]: (... ![X]: ...) +-- OK: (![X]: ...) & (![X]: ...) +-- Free variables must also not be bound inside subformulae +data Form + = Literal Literal + | Not Form + | And (Seq Form) + | Or (Seq Form) + | Equiv Form Form + | ForAll {-# UNPACK #-} !(Bind Form) + | Exists {-# UNPACK #-} !(Bind Form) + -- Just exists so that parsing followed by pretty-printing is + -- somewhat lossless; the simplify function will get rid of it + | Connective Connective Form Form + +-- Miscellaneous connectives that exist in TPTP +data Connective = Implies | Follows | Xor | Nor | Nand + +connective :: Connective -> Form -> Form -> Form +connective Implies t u = nt t \/ u +connective Follows t u = t \/ nt u +connective Xor t u = nt (t `Equiv` u) +connective Nor t u = nt (t \/ u) +connective Nand t u = nt (t /\ u) + +data Bind a = Bind (NameMap Variable) a + +true, false :: Form +true = And S.Nil +false = Or S.Nil + +isTrue, isFalse :: Form -> Bool +isTrue (And S.Nil) = True +isTrue _ = False +isFalse (Or S.Nil) = True +isFalse _ = False + +nt :: Form -> Form +nt (Not a) = a +nt a = Not a + +(.=>.) :: Form -> Form -> Form +(.=>.) = connective Implies + +(.=.) :: Term -> Term -> Form +t .=. u | typ t == O = Literal (Pos (Tru t)) `Equiv` Literal (Pos (Tru u)) + | otherwise = Literal (Pos (t :=: u)) + +(/\), (\/) :: Form -> Form -> Form +And as /\ And bs = And (as `S.append` bs) +a /\ b | isFalse a || isFalse b = false +And as /\ b = And (b `S.cons` as) +a /\ And bs = And (a `S.cons` bs) +a /\ b = And (S.Unit a `S.append` S.Unit b) + +Or as \/ Or bs = Or (as `S.append` bs) +a \/ b | isTrue a || isTrue b = true +Or as \/ b = Or (b `S.cons` as) +a \/ Or bs = Or (a `S.cons` bs) +a \/ b = Or (S.Unit a `S.append` S.Unit b) + +closeForm :: Form -> Form +closeForm f | Map.null vars = f + | otherwise = ForAll (Bind vars f) + where vars = free f + +conj, disj :: S.List f => f Form -> Form +conj = And . S.fromList +disj = Or . S.fromList + +-- remove Not from the root of a problem +positive :: Form -> Form +positive (Not f) = notInwards f +-- Some connectives are fairly not-ish +positive (Connective c t u) = positive (connective c t u) +positive f = f + +notInwards :: Form -> Form +notInwards (And as) = Or (fmap notInwards as) +notInwards (Or as) = And (fmap notInwards as) +notInwards (a `Equiv` b) = notInwards a `Equiv` b +notInwards (Not a) = positive a +notInwards (ForAll (Bind vs a)) = Exists (Bind vs (notInwards a)) +notInwards (Exists (Bind vs a)) = ForAll (Bind vs (notInwards a)) +notInwards (Literal l) = Literal (neg l) +notInwards (Connective c t u) = notInwards (connective c t u) + +-- remove Exists and Or from the top level of a formula +simple :: Form -> Form +simple (Or as) = Not (And (fmap nt as)) +simple (Exists (Bind vs a)) = Not (ForAll (Bind vs (nt a))) +simple (Connective c t u) = simple (connective c t u) +simple a = a + +-- perform some easy algebraic simplifications +simplify t@Literal{} = t +simplify (Connective c t u) = simplify (connective c t u) +simplify (Not t) = simplify (notInwards t) +simplify (And ts) = S.fold (/\) id true (fmap simplify ts) +simplify (Or ts) = S.fold (\/) id false (fmap simplify ts) +simplify (Equiv t u) = equiv (simplify t) (simplify u) + where equiv t u | isTrue t = u + | isTrue u = t + | isFalse t = nt u + | isFalse u = nt t + | otherwise = Equiv t u +simplify (ForAll (Bind vs t)) = forAll vs (simplify t) + where forAll vs t | Map.null vs = t + forAll vs (ForAll (Bind vs' t)) = ForAll (Bind (Map.union vs vs') t) + forAll vs t = ForAll (Bind vs t) +simplify (Exists (Bind vs t)) = exists vs (simplify t) + where exists vs t | Map.null vs = t + exists vs (Exists (Bind vs' t)) = Exists (Bind (Map.union vs vs') t) + exists vs t = Exists (Bind vs t) + +---------------------------------------------------------------------- +-- Clauses + +type CNF = Closed Obligs + +data Obligs = Obligs { + axioms :: [Input Clause], + conjectures :: [[Input Clause]], + satisfiable :: String, + unsatisfiable :: String + } + +toObligs :: [Input Clause] -> [[Input Clause]] -> Obligs +toObligs axioms [] = Obligs axioms [[]] "Satisfiable" "Unsatisfiable" +toObligs axioms [conjecture] = Obligs axioms [conjecture] "CounterSatisfiable" "Theorem" +toObligs axioms conjectures = Obligs axioms conjectures "GaveUp" "Theorem" + +newtype Clause = Clause (Bind [Literal]) + +clause :: S.List f => f (Signed Atomic) -> Clause +clause xs = Clause (bind (S.toList xs)) + +toForm :: Clause -> Form +toForm (Clause (Bind vs ls)) = ForAll (Bind vs (Or (S.fromList (map Literal ls)))) + +toLiterals :: Clause -> [Literal] +toLiterals (Clause (Bind _ ls)) = ls + +---------------------------------------------------------------------- +-- Problems + +type Tag = BS.ByteString + +data Kind = Axiom | Conjecture | Question deriving (Eq, Ord) + +data Answer = Satisfiable | Unsatisfiable | NoAnswer NoAnswerReason + deriving (Eq, Ord) + +instance Show Answer where + show Satisfiable = "Satisfiable" + show Unsatisfiable = "Unsatisfiable" + show (NoAnswer x) = show x + +data NoAnswerReason = GaveUp | Timeout deriving (Eq, Ord, Show) + +data Input a = Input + { tag :: Tag, + kind :: Kind, + what :: a } + +type Problem a = Closed [Input a] + +instance Functor Input where + fmap f x = x { what = f (what x) } + +---------------------------------------------------------------------- +-- Symbolic stuff + +-- A universe of types with typecase +data TypeOf a where + Form :: TypeOf Form + Clause_ :: TypeOf Clause + Term :: TypeOf Term + Atomic :: TypeOf Atomic + Signed :: (Symbolic a, Symbolic (Signed a)) => TypeOf (Signed a) + Bind_ :: (Symbolic a, Symbolic (Bind a)) => TypeOf (Bind a) + List :: (Symbolic a, Symbolic [a]) => TypeOf [a] + Seq :: (Symbolic a, Symbolic (Seq a)) => TypeOf (Seq a) + Input_ :: (Symbolic a, Symbolic (Input a)) => TypeOf (Input a) + Obligs_ :: TypeOf Obligs + +class Symbolic a where + typeOf :: a -> TypeOf a + +instance Symbolic Form where typeOf _ = Form +instance Symbolic Clause where typeOf _ = Clause_ +instance Symbolic Term where typeOf _ = Term +instance Symbolic Atomic where typeOf _ = Atomic +instance Symbolic a => Symbolic (Signed a) where typeOf _ = Signed +instance Symbolic a => Symbolic (Bind a) where typeOf _ = Bind_ +instance Symbolic a => Symbolic [a] where typeOf _ = List +instance Symbolic a => Symbolic (Seq a) where typeOf _ = Seq +instance Symbolic a => Symbolic (Input a) where typeOf _ = Input_ +instance Symbolic Obligs where typeOf _ = Obligs_ + +-- Generic representations of values. +data Rep a where + Const :: !a -> Rep a + Unary :: Symbolic a => (a -> b) -> a -> Rep b + Binary :: (Symbolic a, Symbolic b) => (a -> b -> c) -> a -> b -> Rep c + +-- This inline declaration is crucial so that +-- pattern-matching on a rep degenerates into typecase. +{-# INLINE rep #-} +rep :: Symbolic a => a -> Rep a +rep x = + case typeOf x of + Form -> rep' x + Clause_ -> rep' x + Term -> rep' x + Atomic -> rep' x + Signed -> rep' x + Bind_ -> rep' x + List -> rep' x + Seq -> rep' x + Input_ -> rep' x + Obligs_ -> rep' x + +-- Implementation of rep for all types +class Unpack a where + rep' :: a -> Rep a + +instance Unpack Form where + rep' (Literal l) = Unary Literal l + rep' (Not t) = Unary Not t + rep' (And ts) = Unary And ts + rep' (Or ts) = Unary Or ts + rep' (Equiv t u) = Binary Equiv t u + rep' (ForAll b) = Unary ForAll b + rep' (Exists b) = Unary Exists b + rep' (Connective c t u) = Binary (Connective c) t u + +instance Unpack Clause where + rep' (Clause ls) = Unary Clause ls + +instance Unpack Term where + rep' t@Var{} = Const t + rep' (f :@: ts) = Unary (f :@:) ts + +instance Unpack Atomic where + rep' (t :=: u) = Binary (:=:) t u + rep' (Tru p) = Unary Tru p + +instance Symbolic a => Unpack (Signed a) where + rep' (Pos x) = Unary Pos x + rep' (Neg x) = Unary Neg x + +instance Symbolic a => Unpack (Bind a) where + rep' (Bind vs x) = Unary (Bind vs) x + +instance Symbolic a => Unpack [a] where + rep' [] = Const [] + rep' (x:xs) = Binary (:) x xs + +instance Symbolic a => Unpack (Seq a) where + rep' S.Nil = Const S.Nil + rep' (S.Unit x) = Unary S.Unit x + rep' (S.Append x y) = Binary S.Append x y + +instance Symbolic a => Unpack (Input a) where + rep' (Input tag kind what) = Unary (Input tag kind) what + +instance Unpack Obligs where + rep' (Obligs ax conj s1 s2) = + Binary (\ax' conj' -> Obligs ax' conj' s1 s2) ax conj + +-- Little generic strategies + +{-# INLINE recursively #-} +recursively :: Symbolic a => (forall a. Symbolic a => a -> a) -> a -> a +recursively h t = + case rep t of + Const x -> x + Unary f x -> f (h x) + Binary f x y -> f (h x) (h y) + +{-# INLINE recursivelyM #-} +recursivelyM :: (Monad m, Symbolic a) => (forall a. Symbolic a => a -> m a) -> a -> m a +recursivelyM h t = + case rep t of + Const x -> return x + Unary f x -> liftM f (h x) + Binary f x y -> liftM2 f (h x) (h y) + +{-# INLINE collect #-} +collect :: (Symbolic a, Monoid b) => (forall a. Symbolic a => a -> b) -> a -> b +collect h t = + case rep t of + Const x -> mempty + Unary f x -> h x + Binary f x y -> h x `mappend` h y + +---------------------------------------------------------------------- +-- Substitutions + +type Subst = NameMap (Name ::: Term) + +ids :: Subst +ids = Map.empty + +(|=>) :: Named a => a -> Term -> Subst +v |=> x = NameMap.singleton (name v ::: x) + +(|+|) :: Subst -> Subst -> Subst +(|+|) = Map.union + +subst :: Symbolic a => Subst -> a -> a +subst s t = + case typeOf t of + Term -> term t + Bind_ -> bind t + _ -> generic t + where + term (Var x) + | Just u <- NameMap.lookup (name x) s = rhs u + term t = generic t + + bind :: Symbolic a => Bind a -> Bind a + bind (Bind vs t) = + Bind vs (subst (checkBinder vs (s Map.\\ vs)) t) + + generic :: Symbolic a => a -> a + generic t = recursively (subst s) t + +---------------------------------------------------------------------- +-- Functions operating on symbolic terms + +free :: Symbolic a => a -> NameMap Variable +free t + | Term <- typeOf t, + Var x <- t = var x + | Bind_ <- typeOf t = bind t + | otherwise = collect free t + where + var :: Variable -> NameMap Variable + var x = NameMap.singleton x + + bind :: Symbolic a => Bind a -> NameMap Variable + bind (Bind vs t) = free t Map.\\ vs + +ground :: Symbolic a => a -> Bool +ground = Map.null . free + +bind :: Symbolic a => a -> Bind a +bind x = Bind (free x) x + +-- Helper function for collecting information from terms and binders. +termsAndBinders :: forall a b. + Symbolic a => + (Term -> Seq b) -> + (forall a. Symbolic a => Bind a -> Seq b) -> + a -> Seq b +termsAndBinders term bind = aux where + aux :: Symbolic c => c -> Seq b + aux t = + collect aux t `S.append` + case typeOf t of + Term -> term t + Bind_ -> bind t + _ -> S.Nil + +names :: Symbolic a => a -> [Name] +names = nub . termsAndBinders term bind where + term t = return (name t) `mappend` return (name (typ t)) + + bind :: Symbolic a => Bind a -> Seq Name + bind (Bind vs _) = S.fromList (map name (NameMap.toList vs)) + +types :: Symbolic a => a -> [Type] +types = nub . termsAndBinders term bind where + term t = return (typ t) + + bind :: Symbolic a => Bind a -> Seq Type + bind (Bind vs _) = S.fromList (map typ (NameMap.toList vs)) + +types' :: Symbolic a => a -> [Type] +types' = filter (/= O) . types + +terms :: Symbolic a => a -> [Term] +terms = nub . termsAndBinders term mempty where + term t = return t + +vars :: Symbolic a => a -> [Variable] +vars = nub . termsAndBinders term bind where + term (Var x) = return x + term _ = mempty + + bind :: Symbolic a => Bind a -> Seq Variable + bind (Bind vs _) = S.fromList (NameMap.toList vs) + +functions :: Symbolic a => a -> [Function] +functions = nub . termsAndBinders term mempty where + term (f :@: _) = return f + term _ = mempty + +isFof :: Symbolic a => a -> Bool +isFof f = length (types' f) <= 1 + +uniqueNames :: Symbolic a => a -> NameM a +uniqueNames t = evalStateT (aux Map.empty t) (free t) + where aux :: Symbolic a => Subst -> a -> StateT (NameMap Variable) NameM a + aux s t = + case typeOf t of + Term -> term s t + Bind_ -> bind s t + _ -> generic s t + + term :: Subst -> Term -> StateT (NameMap Variable) NameM Term + term s t@(Var x) = do + case NameMap.lookup (name x) s of + Nothing -> return t + Just (_ ::: u) -> return u + term s t = generic s t + + bind :: Symbolic a => Subst -> Bind a -> StateT (NameMap Variable) NameM (Bind a) + bind s (Bind vs x) = do + used <- get + let (stale, fresh) = partition (`NameMap.member` used) (NameMap.toList vs) + stale' <- sequence [ lift (newSymbol x t) | x ::: t <- stale ] + put (used `Map.union` NameMap.fromList fresh `Map.union` NameMap.fromList stale') + case stale of + [] -> fmap (Bind vs) (aux s x) + _ -> + do + let s' = NameMap.fromList [name x ::: Var y | (x, y) <- stale `zip` stale'] `Map.union` s + vs' = NameMap.fromList (stale' ++ fresh) + fmap (Bind vs') (aux s' x) + + generic :: Symbolic a => Subst -> a -> StateT (NameMap Variable) NameM a + generic s t = recursivelyM (aux s) t + +-- Force a value. +force :: Symbolic a => a -> a +force x = rnf x `seq` x + where rnf :: Symbolic a => a -> () + rnf x = + case rep x of + Const !_ -> () + Unary _ x -> rnf x + Binary _ x y -> rnf x `seq` rnf y + +-- Check that there aren't two nested binders binding the same variable +check :: Symbolic a => a -> a +check x | not debugging = x + | check' (free x) x = x + | otherwise = error "Form.check: invariant broken" + where check' :: Symbolic a => NameMap Variable -> a -> Bool + check' vars t = + case typeOf t of + Term -> term vars t + Bind_ -> bind vars t + _ -> generic vars t + + term :: NameMap Variable -> Term -> Bool + term vars (Var x) = x `NameMap.member` vars + term vars t = generic vars t + + bind :: Symbolic a => NameMap Variable -> Bind a -> Bool + bind vars (Bind vs t) = + Map.null (vs `Map.intersection` vars) && + check' (vs `Map.union` vars) t + + generic :: Symbolic a => NameMap Variable -> a -> Bool + generic vars = getAll . collect (All . generic vars) + +-- Check that a binder doesn't capture variables from a substitution. +checkBinder :: NameMap Variable -> Subst -> Subst +checkBinder vs s | not debugging = s + | Map.null (free [ t | _ ::: t <- NameMap.toList s ] `Map.intersection` vs) = s + | otherwise = error "Form.checkBinder: capturing substitution" + +-- Reestablish sharing in a formula. +type ShareState = (NameMap Type, NameMap Variable, NameMap Function) + +share :: Symbolic a => a -> a +share x = evalState (shareM x) initial + where initial :: ShareState + initial = (Map.empty, Map.empty, Map.empty) + + shareM :: Symbolic a => a -> State ShareState a + shareM t = + case typeOf t of + Term -> term t + Bind_ -> bind t + _ -> recursivelyM shareM t + + bind :: Symbolic a => Bind a -> State ShareState (Bind a) + bind (Bind vs x) = + liftM2 Bind (mapM var vs) (shareM x) + + term :: Term -> State ShareState Term + term (Var x) = fmap Var (var x) + term (f :@: ts) = liftM2 (:@:) (fun f) (mapM term ts) + + fun :: Function -> State ShareState Function + fun (f ::: FunType args res) = do + args' <- mapM type_ args + res' <- type_ res + memo funAccessor (f ::: FunType args' res') + + var :: Variable -> State ShareState Variable + var (x ::: ty) = fmap (x :::) (type_ ty) >>= memo varAccessor + + type_ :: Type -> State ShareState Type + type_ = memo typeAccessor + + typeAccessor = (\(x, y, z) -> x, \x (_, y, z) -> (x, y, z)) + varAccessor = (\(x, y, z) -> y, \y (x, _, z) -> (x, y, z)) + funAccessor = (\(x, y, z) -> z, \z (x, y, _) -> (x, y, z)) + + memo :: Named a => + (ShareState -> NameMap a, + NameMap a -> ShareState -> ShareState) -> + a -> State ShareState a + memo (get_, put_) x = do + m <- gets get_ + case NameMap.lookup (name x) m of + Nothing -> do + modify (put_ (NameMap.insert x m)) + return x + Just y -> + return y + +-- Apply a function to each type, while preserving sharing. +mapType :: Symbolic a => (Type -> Type) -> a -> a +mapType f = share . mapType' + where mapType' :: Symbolic a => a -> a + mapType' t = + case typeOf t of + Term -> term t + Bind_ -> bind t + _ -> recursively mapType' t + + bind :: Symbolic a => Bind a -> Bind a + bind (Bind vs t) = Bind (fmap var vs) (mapType' t) + + term (f :@: ts) = fun f :@: map term ts + term (Var x) = Var (var x) + + var (x ::: ty) = x ::: f ty + fun (x ::: FunType args res) = x ::: FunType (map f args) (f res) diff --git a/Jukebox/GuessModel.hs b/Jukebox/GuessModel.hs new file mode 100644 --- /dev/null +++ b/Jukebox/GuessModel.hs @@ -0,0 +1,121 @@ +{-# LANGUAGE GADTs, PatternGuards #-} +module Jukebox.GuessModel where + +import Control.Monad +import qualified Data.ByteString.Char8 as BS +import Jukebox.Name +import Jukebox.Form +import Jukebox.Clausify hiding (cnf) +import Jukebox.TPTP.Print +import Jukebox.TPTP.ParseSnippet +import Jukebox.Utils + +data Universe = Peano | Trees + +universe :: Universe -> Type -> NameM ([Function], [Form]) +universe Peano = peano +universe Trees = trees + +peano i = do + zero <- newFunction "zero" [] i + succ <- newFunction "succ" [i] i + pred <- newFunction "pred" [i] i + let types = [("$i", i)] + funs = [("zero", zero), + ("succ", succ), + ("pred", pred)] + + prelude <- mapM (cnf types funs) [ + "zero != succ(X)", + "pred(succ(X)) = X" + ] + return ([zero, succ], prelude) + +trees i = do + nil <- newFunction "nil" [] i + bin <- newFunction "bin" [i, i] i + left <- newFunction "left" [i] i + right <- newFunction "right" [i] i + let types = [("$i", i)] + funs = [("nil", nil), + ("bin", bin), + ("left", left), + ("right", right)] + + prelude <- mapM (cnf types funs) [ + "nil != bin(X,Y)", + "left(bin(X,Y)) = X", + "right(bin(X,Y)) = Y" + ] + return ([nil, bin], prelude) + +guessModel :: [String] -> Universe -> Problem Form -> Problem Form +guessModel expansive univ prob = close prob $ \forms -> do + let i = ind forms + answerType <- newType "answer" + answer <- newFunction "$answer" [answerType] O + let withExpansive f func = f func (BS.unpack (base (name func)) `elem` expansive) answer + (constructors, prelude) <- universe univ i + program <- fmap concat (mapM (withExpansive (function constructors)) (functions forms)) + return (map (Input (BS.pack "adt") Axiom) prelude ++ + map (Input (BS.pack "program") Axiom) program ++ + forms) + +ind :: Symbolic a => a -> Type +ind x = + case types' x of + [ty] -> ty + [] -> Type nameI Infinite Infinite + _ -> error "GuessModel: can't deal with many-typed problems" + +function :: [Function] -> Function -> Bool -> Function -> NameM [Form] +function constructors f expansive answerP = fmap concat $ do + argss <- cases constructors (funArgs f) + forM argss $ \args -> do + fname <- newFunction ("exhausted_" ++ BS.unpack (base (name f)) ++ "_case") + [] (head (funArgs answerP)) + let answer = Literal (Pos (Tru (answerP :@: [fname :@: []]))) + let theRhss = rhss constructors args f expansive answer + alts <- forM theRhss $ \rhs -> do + pred <- newFunction (concat (lines (prettyFormula rhs))) [] O + return (Literal (Pos (Tru (pred :@: [])))) + return $ + disj alts: + [ closeForm (Connective Implies alt rhs) + | (alt, rhs) <- zip alts theRhss ] + +rhss :: [Function] -> [Term] -> Function -> Bool -> Form -> [Form] +rhss constructors args f expansive answer = + case typ f of + O -> + Literal (Pos (Tru (f :@: args))): + Literal (Neg (Tru (f :@: args))): + map its (map (f :@:) (recursive args)) + _ | expansive -> map its (usort (unconditional ++ constructor)) + | otherwise -> map its (usort unconditional) ++ [answer] + where recursive [] = [] + recursive (a:as) = reduce a ++ map (a:) (recursive as) + where reduce (f :@: xs) = [ x:as' | x <- xs, as' <- as:recursive as ] + reduce _ = [] + constructor = [ c :@: xs + | c <- constructors, + xs <- sequence (replicate (arity c) unconditional) ] + + subterm = terms args + its t = f :@: args .=. t + unconditional = map (f :@:) (recursive args) ++ subterm + +cases :: [Function] -> [Type] -> NameM [[Term]] +cases constructors [] = return [[]] +cases constructors (ty:tys) = do + ts <- cases1 constructors ty + tss <- cases constructors tys + return (liftM2 (:) ts tss) + +cases1 :: [Function] -> Type -> NameM [Term] +cases1 constructors ty = do + let maxArity = maximum (map arity constructors) + varNames = take maxArity (cycle ["X", "Y", "Z"]) + vars <- mapM (flip newSymbol ty) varNames + return [ c :@: take (arity c) (map Var vars) + | c <- constructors ] diff --git a/Jukebox/HighSat.hs b/Jukebox/HighSat.hs new file mode 100644 --- /dev/null +++ b/Jukebox/HighSat.hs @@ -0,0 +1,113 @@ +{-# LANGUAGE BangPatterns, GeneralizedNewtypeDeriving #-} +module Jukebox.HighSat where + +import MiniSat hiding (neg) +import qualified MiniSat +import qualified Jukebox.Seq as Seq +import Jukebox.Seq(Seq, List) +import Jukebox.Form(Signed(..), neg) +import qualified Jukebox.Map as Map +import Jukebox.Map(Map) +import Control.Monad.State.Strict +import Control.Monad.Reader +import Control.Monad.Trans +import Data.Hashable +import Data.Traversable hiding (mapM, sequence) +import Control.Applicative +import Data.Maybe +import Data.List(partition) + +newtype Sat1 a b = Sat1 { runSat1_ :: ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b } deriving (Functor, Monad, MonadIO) +newtype Sat a b c = Sat { runSat_ :: ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c } deriving (Functor, Monad, MonadIO) +data SatState a = SatState Solver (Map a Lit) +type Watch a = a -> Sat1 a () + +data Form a + = Lit (Signed a) + | And (Seq (Form a)) + | Or (Seq (Form a)) + +nt :: Form a -> Form a +nt (Lit x) = Lit (neg x) +nt (And xs) = Or (fmap nt xs) +nt (Or xs) = And (fmap nt xs) + +conj, disj :: List f => f (Form a) -> Form a +conj = And . Seq.fromList +disj = Or . Seq.fromList + +true, false :: Form a +true = And Seq.Nil +false = Or Seq.Nil + +unique :: List f => f (Form a) -> Form a +unique = u . Seq.toList + where u [x] = true + u (x:xs) = conj [disj [nt x, conj (map nt xs)], + u xs] + +runSat :: (Hashable b, Ord b) => Watch a -> [b] -> Sat a b c -> IO c +runSat w idxs x = go idxs Map.empty + where go [] m = evalStateT (runReaderT (runSat_ x) w) m + go (idx:idxs) m = + withNewSolver $ \s -> go idxs (Map.insert idx (SatState s Map.empty) m) + +runSat1 :: (Ord a, Hashable a) => Watch a -> Sat1 a b -> IO b +runSat1 w x = runSat w [()] (atIndex () x) + +atIndex :: (Ord a, Hashable a, Ord b, Hashable b) => b -> Sat1 a c -> Sat a b c +atIndex !idx m = do + watch <- Sat ask + SatState s ls <- Sat (gets (Map.findWithDefault (error "withSolver: index not found") idx)) + (x, ls') <- liftIO (runStateT (runReaderT (runReaderT (runSat1_ m) s) watch) ls) + Sat (modify (Map.insert idx (SatState s ls'))) + return x + +solve :: (Ord a, Hashable a) => [Signed a] -> Sat1 a Bool +solve xs = do + s <- Sat1 ask + ls <- mapM lit xs + liftIO (MiniSat.solve s ls) + +model :: (Ord a, Hashable a) => Sat1 a (a -> Bool) +model = do + s <- Sat1 ask + m <- Sat1 (lift get) + vals <- liftIO (traverse (MiniSat.modelValue s) m) + return (\v -> fromMaybe False (Map.findWithDefault Nothing v vals)) + +modelValue :: (Ord a, Hashable a) => a -> Sat1 a Bool +modelValue x = do + s <- Sat1 ask + l <- var x + Just b <- liftIO (MiniSat.modelValue s l) + return b + +addForm :: (Ord a, Hashable a) => Form a -> Sat1 a () +addForm f = do + s <- Sat1 ask + cs <- flatten f + liftIO (Seq.mapM (MiniSat.addClause s . Seq.toList) cs) + return () + +flatten :: (Ord a, Hashable a) => Form a -> Sat1 a (Seq (Seq Lit)) +flatten (Lit l) = fmap (Seq.Unit . Seq.Unit) (lit l) +flatten (And fs) = fmap Seq.concat (Seq.mapM flatten fs) +flatten (Or fs) = fmap (fmap Seq.concat . Seq.sequence) (Seq.mapM flatten fs) + +lit :: (Ord a, Hashable a) => Signed a -> Sat1 a Lit +lit (Pos x) = var x +lit (Neg x) = liftM MiniSat.neg (var x) + +var :: (Ord a, Hashable a) => a -> Sat1 a Lit +var x = do + s <- Sat1 ask + m <- Sat1 get + case Map.lookup x m of + Nothing -> do + l <- liftIO (MiniSat.newLit s) + Sat1 (put (Map.insert x l m)) + w <- Sat1 (lift ask) + w x + return l + Just l -> return l diff --git a/Jukebox/InferTypes.hs b/Jukebox/InferTypes.hs new file mode 100644 --- /dev/null +++ b/Jukebox/InferTypes.hs @@ -0,0 +1,82 @@ +{-# LANGUAGE TypeOperators, GADTs #-} +module Jukebox.InferTypes where + +import Control.Monad +import Jukebox.Form +import Jukebox.Name +import qualified Jukebox.NameMap as NameMap +import Jukebox.NameMap(NameMap) +import Jukebox.UnionFind hiding (rep) + +type Function' = Name ::: ([Type'], Type') +type Variable' = Name ::: Type' +type Type' = Name ::: Type + +inferTypes :: [Input Clause] -> NameM ([Input Clause], Type -> Type) +inferTypes prob = do + funMap <- + fmap NameMap.fromList . sequence $ + [ do res <- newName (typ f) + args <- mapM newName (funArgs f) + return (name f ::: + (zipWith (:::) args (funArgs f), + res ::: typ f)) + | f <- functions prob ] + varMap <- + fmap NameMap.fromList . sequence $ + [ do ty <- newName (typ v) + return (name v ::: (ty ::: typ v)) + | v <- vars prob ] + + let tyMap = NameMap.fromList $ + concat [ res:args | _ ::: (args, res) <- NameMap.toList funMap ] ++ + [ ty | _ ::: ty <- NameMap.toList varMap ] + + let (prob', rep) = solve funMap varMap prob + rep' ty = rhs (NameMap.lookup_ (rep (name ty)) tyMap) + + return (prob', rep') + +solve :: NameMap Function' -> NameMap Variable' -> + [Input Clause] -> ([Input Clause], Name -> Name) +solve funMap varMap prob = (prob', rep) + where prob' = share (aux prob) + aux :: Symbolic a => a -> a + aux t = + case typeOf t of + Bind_ -> bind t + Term -> term t + _ -> recursively aux t + + bind :: Symbolic a => Bind a -> Bind a + bind (Bind vs t) = Bind (fmap var vs) (aux t) + + term (f :@: ts) = fun f :@: map term ts + term (Var x) = Var (var x) + + fun (f ::: _) = + let (args, res) = rhs (NameMap.lookup_ f funMap) + in f ::: FunType (map type_ args) (type_ res) + + var (x ::: _) = x ::: type_ (rhs (NameMap.lookup_ x varMap)) + + type_ (name ::: _) + | name == nameO = O + | otherwise = Type (rep name) Infinite Infinite + + rep = evalUF initial $ do + generate funMap varMap prob + reps + +generate :: NameMap Function' -> NameMap Variable' -> [Input Clause] -> UF Name () +generate funMap varMap cs = mapM_ (mapM_ atomic) lss + where lss = map (map the . toLiterals . what) cs + atomic (Tru p) = void (term p) + atomic (t :=: u) = do { t' <- term t; u' <- term u; t' =:= u'; return () } + term (Var x) = return y + where _ ::: (y ::: _) = NameMap.lookup_ x varMap + term (f :@: xs) = do + ys <- mapM term xs + let _ ::: (zs, r) = NameMap.lookup_ f funMap + zipWithM_ (=:=) ys (map lhs zs) + return (lhs r) diff --git a/Jukebox/Map.hs b/Jukebox/Map.hs new file mode 100644 --- /dev/null +++ b/Jukebox/Map.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} +module Jukebox.Map where + +import qualified Data.HashMap.Lazy as H + +type Map a b = H.HashMap a b + +fromList = H.fromList +toList = H.toList +insertWith = H.insertWith +empty = H.empty +findWithDefault = H.lookupDefault +lookup = H.lookup +insert = H.insert +delete = H.delete +elems = H.elems +union = H.union +intersection = H.intersection +null = H.null +m ! x = H.lookupDefault (error "Map.!: key not found") x m + +member x m = + case H.lookup x m of + Nothing -> False + Just{} -> True + +m1 \\ m2 = + H.foldrWithKey (\k v m -> H.delete k m) m1 m2 diff --git a/Jukebox/Monotonox/Monotonicity.hs b/Jukebox/Monotonox/Monotonicity.hs new file mode 100644 --- /dev/null +++ b/Jukebox/Monotonox/Monotonicity.hs @@ -0,0 +1,82 @@ +{-# LANGUAGE TypeOperators #-} +module Jukebox.Monotonox.Monotonicity where + +import Prelude hiding (lookup) +import Jukebox.Name +import Jukebox.Form hiding (Form, clause, true, false, conj, disj) +import Jukebox.HighSat +import Jukebox.NameMap as NameMap +import Jukebox.Utils +import Data.Hashable +import Control.Monad + +data Extension = TrueExtend | FalseExtend | CopyExtend deriving Show + +data Var = FalseExtended Function | TrueExtended Function deriving (Eq, Ord) + +instance Hashable Var where + hashWithSalt s = hashWithSalt s . convert + where convert (FalseExtended x) = Left x + convert (TrueExtended x) = Right x + +annotateMonotonicity :: Problem Clause -> IO (Problem Clause) +annotateMonotonicity prob = do + m <- monotone (map what (open prob)) + let f O = O + f ty = + case lookup (name ty) m of + Nothing -> ty + Just{} -> ty { tmonotone = Finite 0 } + return (fmap (mapType f) prob) + +monotone :: [Clause] -> IO (NameMap (Type ::: Maybe (NameMap (Function ::: Extension)))) +monotone cs = runSat watch tys $ do + let fs = functions cs + mapM_ (clause . toLiterals) cs + fmap NameMap.fromList . forM tys $ \ty -> atIndex ty $ do + r <- solve [] + case r of + False -> return (ty ::: Nothing) + True -> do + m <- model + return (ty ::: Just (fromModel fs ty m)) + where watch (FalseExtended f) = + addForm (disj [Lit (Neg (FalseExtended f)), + Lit (Neg (TrueExtended f))]) + watch _ = return () + tys = types' cs + +fromModel :: [Function] -> Type -> (Var -> Bool) -> NameMap (Function ::: Extension) +fromModel fs ty m = NameMap.fromList [ f ::: extension f m | f <- fs, typ f == O, ty `elem` args (rhs f) ] + +extension :: Function -> (Var -> Bool) -> Extension +extension f m = + case (m (FalseExtended f), m (TrueExtended f)) of + (False, False) -> CopyExtend + (True, False) -> FalseExtend + (False, True) -> TrueExtend + +clause :: [Literal] -> Sat Var Type () +clause ls = mapM_ (literal ls) ls + +literal :: [Literal] -> Literal -> Sat Var Type () +literal ls (Pos (t :=: u)) = atIndex (typ t) $ do + addForm (safe ls t) + addForm (safe ls u) +literal ls (Neg (_ :=: _)) = return () +literal ls (Pos (Tru (p :@: ts))) = + forM_ ts $ \t -> atIndex (typ t) $ addForm (disj [safe ls t, Lit (Neg (FalseExtended p))]) +literal ls (Neg (Tru (p :@: ts))) = + forM_ ts $ \t -> atIndex (typ t) $ addForm (disj [safe ls t, Lit (Neg (TrueExtended p))]) + +safe :: [Literal] -> Term -> Form Var +safe ls (Var x) = disj [ guards l x | l <- ls ] +safe _ _ = true + +guards :: Literal -> Variable -> Form Var +guards (Neg (Var _ :=: Var _)) _ = error "Monotonicity.guards: found a variable inequality X!=Y after clausification" +guards (Neg (Var x :=: _)) y | x == y = true +guards (Neg (_ :=: Var x)) y | x == y = true +guards (Pos (Tru (p :@: ts))) x | Var x `elem` ts = Lit (Pos (TrueExtended p)) +guards (Neg (Tru (p :@: ts))) x | Var x `elem` ts = Lit (Pos (FalseExtended p)) +guards _ _ = false diff --git a/Jukebox/Monotonox/ToFOF.hs b/Jukebox/Monotonox/ToFOF.hs new file mode 100644 --- /dev/null +++ b/Jukebox/Monotonox/ToFOF.hs @@ -0,0 +1,191 @@ +{-# LANGUAGE GADTs, PatternGuards #-} +module Jukebox.Monotonox.ToFOF where + +import Jukebox.Clausify(split, removeEquiv, run, withName) +import Jukebox.Name +import qualified Jukebox.NameMap as NameMap +import Jukebox.Form +import Jukebox.Options +import qualified Data.ByteString.Char8 as BS +import Control.Monad hiding (guard) +import Data.Monoid + +data Scheme = Scheme { + makeFunction :: Type -> NameM Function, + scheme1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1 + } + +data Scheme1 = Scheme1 { + forAll :: Bind Form -> Form, + exists :: Bind Form -> Form, + equals :: Term -> Term -> Form, + funcAxiom :: Function -> NameM Form, + typeAxiom :: Type -> NameM Form + } + +guard :: Scheme1 -> (Type -> Bool) -> Input Form -> Input Form +guard scheme mono (Input t k f) = Input t k (aux (pos k) f) + where aux pos (ForAll (Bind vs f)) + | pos = forAll scheme (Bind vs (aux pos f)) + | otherwise = Not (exists scheme (Bind vs (Not (aux pos f)))) + aux pos (Exists (Bind vs f)) + | pos = exists scheme (Bind vs (aux pos f)) + | otherwise = Not (forAll scheme (Bind vs (Not (aux pos f)))) + aux pos (Literal (Pos (t :=: u))) + | not (mono (typ t)) = equals scheme t u + aux pos (Literal (Neg (t :=: u))) + | not (mono (typ t)) = Not (equals scheme t u) + aux pos l@Literal{} = l + aux pos (Not f) = Not (aux (not pos) f) + aux pos (And fs) = And (fmap (aux pos) fs) + aux pos (Or fs) = Or (fmap (aux pos) fs) + aux pos (Equiv _ _) = error "ToFOF.guard: equiv should have been eliminated" + aux pos (Connective _ _ _) = error "ToFOF.guard: connective should have been eliminated" + pos Axiom = True + pos Conjecture = False + +translate, translate1 :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form +translate1 scheme mono f = close f $ \inps -> do + let tys = types inps + funcs = functions inps + -- Hardly any use adding guards if there's only one type. + mono' | length tys == 1 = const True + | otherwise = mono + typeFuncs <- mapM (makeFunction scheme) tys + let typeMap = NameMap.fromList (zipWith (:::) tys typeFuncs) + lookupType ty = + case NameMap.lookup (name ty) typeMap of + Just (_ ::: f) -> f + Nothing -> error "ToFOF.translate: type not found" + scheme1' = scheme1 scheme mono' lookupType + funcAxioms <- mapM (funcAxiom scheme1') funcs + typeAxioms <- mapM (typeAxiom scheme1') tys + let axioms = + map (simplify . ForAll . bind) . split . simplify . foldr (/\) true $ + funcAxioms ++ typeAxioms + return $ + [ Input (BS.pack ("types" ++ show i)) Axiom axiom | (axiom, i) <- zip axioms [1..] ] ++ + map (guard scheme1' mono') inps + +translate scheme mono f = + let f' = + close f $ \inps -> do + forM inps $ \(Input tag kind f) -> do + let prepare f = fmap (foldr (/\) true) (run (withName tag (removeEquiv (simplify f)))) + fmap (Input tag kind) $ + case kind of + Axiom -> prepare f + Conjecture -> fmap notInwards (prepare (nt f)) + typeI = Type nameI (Finite 0) Infinite + in close (translate1 scheme mono f') (return . mapType (const typeI)) + +-- Typing functions. + +tagsFlags :: OptionParser Bool +tagsFlags = + bool "more-axioms" + ["Add extra typing axioms for function arguments,", + "when using typing tags.", + "These are unnecessary for completeness but may help (or hinder!) the prover."] + +tags :: Bool -> Scheme +tags moreAxioms = Scheme + { makeFunction = \ty -> + newFunction (BS.append (BS.pack "to_") (baseName ty)) [ty] ty, + scheme1 = tags1 moreAxioms } + +tags1 :: Bool -> (Type -> Bool) -> (Type -> Function) -> Scheme1 +tags1 moreAxioms mono fs = Scheme1 + { forAll = ForAll, + exists = \(Bind vs f) -> + let bound = foldr (/\) true (map guard (NameMap.toList vs)) + guard v | mono (typ v) = true + | otherwise = Literal (Pos (fs (typ v) :@: [Var v] :=: Var v)) + in Exists (Bind vs (simplify bound /\ f)), + equals = + \t u -> + let protect t@Var{} = fs (typ t) :@: [t] + protect t = t + in Literal (Pos (protect t :=: protect u)), + funcAxiom = tagsAxiom moreAxioms mono fs, + typeAxiom = \ty -> if moreAxioms then tagsAxiom False mono fs (fs ty) else tagsExists mono ty (fs ty) } + +tagsAxiom :: Bool -> (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form +tagsAxiom moreAxioms mono fs f@(_ ::: FunType args res) = do + vs <- forM args $ \ty -> + fmap Var (newSymbol "X" ty) + let t = f :@: vs + at n f xs = take n xs ++ [f (xs !! n)] ++ drop (n+1) xs + tag t = fs (typ t) :@: [t] + equate (ty, t') | mono ty = true + | otherwise = t `eq` t' + t `eq` u | typ t == O = Literal (Pos (Tru t)) `Equiv` Literal (Pos (Tru u)) + | otherwise = Literal (Pos (t :=: u)) + ts = (typ t, tag t): + [ (typ (vs !! n), f :@: at n tag vs) + | moreAxioms, + n <- [0..length vs-1] ] + return (foldr (/\) true (map equate ts)) + +tagsExists :: (Type -> Bool) -> Type -> Function -> NameM Form +tagsExists mono ty f + | mono ty = return true + | otherwise = do + v <- fmap Var (newSymbol "X" ty) + return (Exists (bind (Literal (Pos (f :@: [v] :=: v))))) + +-- Typing predicates. + +guards :: Scheme +guards = Scheme + { makeFunction = \ty -> + newFunction (BS.append (BS.pack "is_") (baseName ty)) [ty] O, + scheme1 = guards1 } + +guards1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1 +guards1 mono ps = Scheme1 + { forAll = \(Bind vs f) -> + let bound = foldr (/\) true (map guard (NameMap.toList vs)) + guard v | mono (typ v) = true + | not (naked True v f) = true + | otherwise = Literal (Pos (Tru (ps (typ v) :@: [Var v]))) + in ForAll (Bind vs (simplify (Not bound) \/ f)), + exists = \(Bind vs f) -> + let bound = foldr (/\) true (map guard (NameMap.toList vs)) + guard v | mono (typ v) = true + | not (naked True v f) = true + | otherwise = Literal (Pos (Tru (ps (typ v) :@: [Var v]))) + in Exists (Bind vs (simplify bound /\ f)), + equals = \t u -> Literal (Pos (t :=: u)), + funcAxiom = guardsAxiom mono ps, + typeAxiom = guardsTypeAxiom mono ps } + +naked :: Symbolic a => Bool -> Variable -> a -> Bool +naked pos v f + | Form <- typeOf f, + Not f' <- f = naked (not pos) v f' + | Signed <- typeOf f, + Pos f' <- f = naked pos v f' + | Signed <- typeOf f, + Neg f' <- f = naked (not pos) v f' + | Atomic <- typeOf f, + t :=: u <- f, + pos = t == Var v || u == Var v + | Bind_ <- typeOf f, + Bind vs f' <- f = not (NameMap.member v vs) && naked pos v f' + | otherwise = getAny (collect (Any . naked pos v) f) + +guardsAxiom :: (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form +guardsAxiom mono ps f@(_ ::: FunType args res) + | mono res = return true + | otherwise = do + vs <- forM args $ \ty -> + fmap Var (newSymbol "X" ty) + return (Literal (Pos (Tru (ps res :@: [f :@: vs])))) + +guardsTypeAxiom :: (Type -> Bool) -> (Type -> Function) -> Type -> NameM Form +guardsTypeAxiom mono ps ty + | mono ty = return true + | otherwise = do + v <- fmap Var (newSymbol "X" ty) + return (Exists (bind (Literal (Pos (Tru (ps ty :@: [v])))))) diff --git a/Jukebox/Name.hs b/Jukebox/Name.hs new file mode 100644 --- /dev/null +++ b/Jukebox/Name.hs @@ -0,0 +1,152 @@ +{-# LANGUAGE TypeOperators, GeneralizedNewtypeDeriving, FlexibleInstances, DeriveDataTypeable #-} +module Jukebox.Name( + Name, uniqueId, base, + stringBaseName, + unsafeMakeName, + (:::)(..), lhs, rhs, + Named(..), + Closed, close, close_, closedIO, open, closed0, stdNames, nameO, nameI, NameM, newName, + unsafeClose, maxIndex, supply, + uniquify) where + +import qualified Data.ByteString.Char8 as BS +import Data.Hashable +import qualified Jukebox.Map as Map +import Jukebox.Utils +import Data.List +import Data.Ord +import Data.Int +import Data.Typeable +import Control.Monad.State.Strict + +data Name = + Name { + uniqueId :: {-# UNPACK #-} !Int64, + base :: BS.ByteString } deriving Typeable + +unsafeMakeName = Name + +instance Eq Name where + x == y = uniqueId x == uniqueId y + +instance Ord Name where + compare = comparing uniqueId + +instance Hashable Name where + hashWithSalt s = hashWithSalt s . uniqueId + +instance Show Name where + show Name { uniqueId = uniqueId, base = base } = + BS.unpack base ++ show uniqueId + +class Named a where + name :: a -> Name + baseName :: a -> BS.ByteString + baseName = base . name + +stringBaseName :: Named a => a -> String +stringBaseName = BS.unpack . baseName + +instance Named BS.ByteString where + name = error "Name.name: used a ByteString as a name" + baseName = id + +instance Named [Char] where + name = error "Name.name: used a String as a name" + baseName = BS.pack + +instance Named Name where + name = id + +data a ::: b = !a ::: !b deriving (Show, Typeable) + +lhs :: (a ::: b) -> a +lhs (x ::: _) = x + +rhs :: (a ::: b) -> b +rhs (_ ::: y) = y + +instance Named a => Eq (a ::: b) where s == t = name s == name t +instance Named a => Ord (a ::: b) where compare = comparing name +instance Named a => Hashable (a ::: b) where hashWithSalt s = hashWithSalt s . name + +instance Named a => Named (a ::: b) where + name (a ::: b) = name a + +newtype NameM a = + NameM { unNameM :: State Int64 a } + deriving (Functor, Monad) + +newName :: Named a => a -> NameM Name +newName x = NameM $ do + idx <- get + let idx'= idx+1 + when (idx' < 0) $ error "Name.newName: too many names" + put $! idx' + return $! Name idx' (baseName x) + +data Closed a = + Closed { + maxIndex :: {-# UNPACK #-} !Int64, + open :: !a } deriving Typeable + +unsafeClose = Closed + +instance Functor Closed where + fmap f (Closed m x) = Closed m (f x) + +closed0 :: Closed () +nameO, nameI :: Name + +closed0 = close_ stdNames (return ()) +[nameO, nameI] = open stdNames + +stdNames :: Closed [Name] +stdNames = close (Closed 0 ["$o", "$i"]) (mapM newName) + +close :: Closed a -> (a -> NameM b) -> Closed b +close Closed{ maxIndex = maxIndex, open = open } f = + let (open', maxIndex') = runState (unNameM (f open)) maxIndex + in Closed{ maxIndex = maxIndex', open = open' } + +close_ :: Closed a -> NameM b -> Closed b +close_ x m = close x (const m) + +closedIO :: Closed (IO a) -> IO (Closed a) +closedIO Closed { maxIndex = maxIndex, open = open } = do + open' <- open + return Closed { maxIndex = maxIndex, open = open' } + +supply :: (Closed () -> Closed a) -> NameM a +supply f = NameM $ do + idx <- get + let res = f (Closed idx ()) + put (maxIndex res) + return (open res) + +uniquify :: [Name] -> (Name -> BS.ByteString) +uniquify xs = f + -- Note to self: nameO should always be mapped to "$o". + -- Therefore we make sure that smaller names have priority + -- over bigger names here. + where + baseMap = + -- Assign numbers to each baseName + fmap (\xs -> Map.fromList (zip (usort xs) [0 :: Int ..])) . + -- Partition by baseName + foldl' (\m x -> Map.insertWith (++) (base x) [x] m) Map.empty $ + xs + f x = combine (base x) b + where + b = Map.findWithDefault (error $ "Name.uniquify: name " ++ show x ++ " not found") x + (Map.findWithDefault (error $ "Name.uniquify: name " ++ show x ++ " not found") (baseName x) baseMap) + combine s 0 = s + combine s n = disambiguate (BS.append s (BS.pack (show n))) + disambiguate s + | not (Map.member s baseMap) = s + | otherwise = + -- Odd situation: we have e.g. a name with baseName "f1", + -- and two names with baseName "f", which would normally + -- become "f" and "f1", but the "f1" conflicts. + -- Try appending some suffix. + disambiguate (BS.snoc s '_') diff --git a/Jukebox/NameMap.hs b/Jukebox/NameMap.hs new file mode 100644 --- /dev/null +++ b/Jukebox/NameMap.hs @@ -0,0 +1,46 @@ +module Jukebox.NameMap(NameMap, lookup, lookup_, insert, member, delete, (!), fromList, toList, singleton) where + +import Prelude hiding (lookup) +import Jukebox.Name +import Jukebox.Map(Map) +import qualified Jukebox.Map as Map +import Data.Int +import qualified Jukebox.Seq as S + +type NameMap a = Map Int64 a + +lookup :: Name -> NameMap a -> Maybe a +lookup x m = Map.lookup (uniqueId x) m + +lookup_ :: Named a => a -> NameMap b -> b +lookup_ x m = + case lookup (name x) m of + Nothing -> error "NameMap.lookup_: key not found" + Just y -> y + +insert :: Named a => a -> NameMap a -> NameMap a +insert x m = Map.insert (uniqueId (name x)) x m + +member :: Named a => a -> NameMap a -> Bool +member x m = keyMember (name x) m + +keyMember :: Name -> NameMap a -> Bool +keyMember x m = Map.member (uniqueId x) m + +delete :: Named a => a -> NameMap a -> NameMap a +delete x m = deleteKey (name x) m + +deleteKey :: Name -> NameMap a -> NameMap a +deleteKey x m = Map.delete (uniqueId x) m + +(!) :: NameMap a -> Name -> a +m ! x = m Map.! uniqueId (name x) + +fromList :: (S.List f, Named a) => f a -> NameMap a +fromList xs = Map.fromList [ (uniqueId (name x), x) | x <- S.toList xs ] + +toList :: NameMap a -> [a] +toList = Map.elems + +singleton :: Named a => a -> NameMap a +singleton x = insert x Map.empty diff --git a/Jukebox/Options.hs b/Jukebox/Options.hs new file mode 100644 --- /dev/null +++ b/Jukebox/Options.hs @@ -0,0 +1,352 @@ +{-# LANGUAGE FlexibleContexts #-} +module Jukebox.Options where + +import Control.Arrow((***)) +import Control.Applicative +import Control.Monad(mplus) +import Data.Char +import Data.List +import Data.Monoid +import System.Environment +import System.Exit +import System.IO + +---------------------------------------------------------------------- +-- A parser of some kind annotated with a help text of some kind +data Annotated d p a = Annotated + { descr :: d, + parser :: p a } + +instance Functor p => Functor (Annotated d p) where + fmap f (Annotated d x) = Annotated d (fmap f x) + +instance (Monoid d, Applicative p) => Applicative (Annotated d p) where + pure = Annotated mempty . pure + Annotated d f <*> Annotated d' x = + Annotated (d `mappend` d') (f <*> x) + +instance (Monoid d, Monoid (p a)) => Monoid (Annotated d p a) where + mempty = Annotated mempty mempty + Annotated d p `mappend` Annotated d' p' = + Annotated (d `mappend` d') (p `mappend` p') + +---------------------------------------------------------------------- +-- Parsing of single arguments (e.g. integers) +-- and single flags (e.g. --verbosity 3). + +type ArgParser = Annotated ArgDesc SeqParser +type ArgDesc = String -- description, e.g. "" + +-- Called SeqParser because <*> is sequential composition. +data SeqParser a = SeqParser + { args :: Int, -- How many arguments will be consumed + consume :: [String] -> Either Error a } + +instance Functor SeqParser where + fmap f (SeqParser a c) = SeqParser a (fmap f . c) + +instance Applicative SeqParser where + pure = SeqParser 0 . const . pure + SeqParser a c <*> SeqParser a' c' = SeqParser (a + a') f + where f xs = c xs <*> c' (drop a xs) + +arg :: ArgDesc -> String -> (String -> Maybe a) -> ArgParser a +arg desc err f = Annotated desc (SeqParser 1 c) + where c [] = Left (Mistake err) + c (x:_) | "--" `isPrefixOf` x = Left (Mistake err) + c (x:_) = + case f x of + Nothing -> Left (Mistake err) + Just ok -> Right ok + +argNum :: (Read a, Num a) => ArgParser a +argNum = arg "" "expected a number" f + where f x = + case reads x of + [(y, "")] -> Just y + _ -> Nothing + +argFile :: ArgParser FilePath +argFile = arg "" "expected a file" Just + +argFiles :: ArgParser [FilePath] +argFiles = arg "" "expected a list of files" $ \x -> + Just $ elts $ x ++ "," + where + elts [] = [] + elts s = w:elts r + where + w = takeWhile (/= ',') s + r = tail (dropWhile (/= ',') s) + +argName :: ArgParser FilePath +argName = arg "" "expected a name" Just + +argNums :: ArgParser [Int] +argNums = arg "" "expected a number list" $ \x -> + nums . groupBy (\x y -> isDigit x == isDigit y) $ x ++ "," + where + nums [] = Just [] + nums (n:",":ns) = (read n :) `fmap` nums ns + nums (n:"..":m:",":ns) = ([read n .. read m] ++) `fmap` nums ns + nums _ = Nothing + +argOption :: [String] -> ArgParser String +argOption as = arg ("<" ++ concat (intersperse " | " as) ++ ">") "expected an argument" elts + where + elts x | x `elem` as = Just x + | otherwise = Nothing + +argList :: [String] -> ArgParser [String] +argList as = arg ("<" ++ concat (intersperse " | " as) ++ ">*") "expected an argument" $ \x -> + elts $ x ++ "," + where + elts [] = Just [] + elts s | w `elem` as = (w:) `fmap` elts r + where + w = takeWhile (/= ',') s + r = tail (dropWhile (/= ',') s) + + elts _ = Nothing + +-- A parser that always fails but produces an error message (useful for --help etc.) +argUsage :: ExitCode -> [String] -> ArgParser a +argUsage code err = Annotated [] (SeqParser 0 (const (Left (Usage code err)))) + +---------------------------------------------------------------------- +-- Parsing of whole command lines. + +type OptionParser = Annotated [Flag] ParParser + +-- Called ParParser because <*> is parallel composition. +-- In other words, in f <*> x, f and x both see the whole command line. +-- We want this when parsing command lines because +-- it doesn't matter what order we write the options in. +data ParParser a = ParParser + { val :: IO a, -- impure so we can put system information in our options records + peek :: [String] -> ParseResult a } + +data ParseResult a + -- Yes n x: consumed n arguments, continue parsing with x + = Yes Int (ParParser a) + -- No x: didn't understand this flag, continue parsing with x + | No (ParParser a) + -- Error + | Error Error + +data Error = + Mistake String + | Usage ExitCode [String] + +instance Functor ParParser where + fmap f x = pure f <*> x + +instance Applicative ParParser where + pure x = ParParser (return x) (const (pure x)) + ParParser v p <*> ParParser v' p' = + ParParser (v <*> v') (\xs -> p xs <*> p' xs) + +instance Functor ParseResult where + fmap f x = pure f <*> x + +instance Applicative ParseResult where + pure = No . pure + Yes n r <*> Yes n' r' + | n == n' = Yes n (r <*> r') + | otherwise = error "Options.ParseResult: inconsistent number of arguments" + Error s <*> _ = Error s + _ <*> Error s = Error s + Yes n r <*> No x = Yes n (r <*> x) + No x <*> Yes n r = Yes n (x <*> r) + No f <*> No x = No (f <*> x) + +runPar :: ParParser a -> [String] -> Either Error (IO a) +runPar p [] = Right (val p) +runPar p xs@(x:_) = + case peek p xs of + Yes n p' -> runPar p' (drop n xs) + No _ -> Left (Mistake ("Didn't recognise option " ++ x)) + Error err -> Left err + +awaitP :: (String -> Bool) -> a -> (String -> [String] -> ParseResult a) -> ParParser a +awaitP p def par = ParParser (return def) f + where f (x:xs) | p x = + case par x xs of + Yes n r -> Yes (n+1) r + No _ -> + error "Options.await: got No" + Error err -> Error err + f _ = No (awaitP p def par) + +await :: String -> a -> ([String] -> ParseResult a) -> ParParser a +await flag def f = awaitP (\x -> "--" ++ flag == x) def (const f) + +data Flag = Flag + { flagName :: String, + flagGroup :: String, + flagHelp :: [String], + flagArgs :: String } deriving (Eq, Show) + +-- From a flag name and and argument parser, produce an OptionParser. +flag :: String -> [String] -> a -> ArgParser a -> OptionParser a +flag name help def (Annotated desc (SeqParser args f)) = + Annotated [desc'] (await name def g) + where desc' = Flag name "Common options" help desc + g xs = + case f xs of + Left (Mistake err) -> Error (Mistake ("Error in option --" ++ name ++ ": " ++ err)) + Left (Usage code err) -> Error (Usage code err) + Right y -> Yes args (pure y <* noFlag) + -- Give an error if the flag is repeated. + noFlag = + await name () + (const (Error (Mistake ("Option --" ++ name ++ " occurred twice")))) + +manyFlags :: String -> [String] -> ArgParser a -> OptionParser [a] +manyFlags name help (Annotated desc (SeqParser args f)) = + fmap reverse (Annotated [desc'] (go [])) + where desc' = Flag name "Common options" help desc + go xs = await name xs (g xs) + g xs ys = + case f ys of + Left (Mistake err) -> Error (Mistake ("Error in option --" ++ name ++ ": " ++ err)) + Left (Usage code err) -> Error (Usage code err) + Right x -> Yes args (go (x:xs)) + +-- Read filenames from the command line. +filenames :: OptionParser [String] +filenames = Annotated [] (from []) + where from xs = awaitP p xs (f xs) + p x = not ("--" `isPrefixOf` x) + f xs y ys = Yes 0 (from (xs ++ [y])) + +-- Take a value from the environment. +io :: IO a -> OptionParser a +io m = Annotated [] p + where p = ParParser m (const (No p)) + +-- A boolean flag. +bool :: String -> [String] -> OptionParser Bool +bool name help = flag name help False (pure True) + +inGroup :: String -> OptionParser a -> OptionParser a +inGroup x (Annotated fls f) = Annotated [fl{ flagGroup = x } | fl <- fls] f + +---------------------------------------------------------------------- +-- Selecting a particular tool. + +type ToolParser = Annotated [Tool] PrefixParser +data Tool = Tool + { toolProgName :: String, + toolName :: String, + toolVersion :: String, + toolHelp :: String } + +newtype PrefixParser a = PrefixParser (String -> Maybe (Tool, ParParser a)) + +instance Functor PrefixParser where + fmap f (PrefixParser g) = PrefixParser (fmap (id *** fmap f) . g) + +instance Monoid (PrefixParser a) where + mempty = PrefixParser (const Nothing) + PrefixParser f `mappend` PrefixParser g = + PrefixParser (\xs -> f xs `mplus` g xs) + +runPref :: PrefixParser a -> [String] -> Either Error (IO a) +runPref _ [] = Left (Mistake "Expected a tool name") +runPref (PrefixParser f) (x:xs) = + case f x of + Nothing -> Left (Mistake ("No such tool " ++ x)) + Just (t, p) -> + case runPar p xs of + Left (Mistake x) -> Left (Usage (ExitFailure 1) (argError t x)) + Left (Usage code x) -> Left (Usage code x) + Right x -> Right x + +tool :: Tool -> OptionParser a -> ToolParser a +tool t p = + Annotated [t] (PrefixParser f) + where f x | x == toolProgName t = Just (t, parser p') + f _ = Nothing + p' = p <* versionParser <* helpParser + helpParser = flag "help" ["Show this help text."] () (argUsage ExitSuccess (help t p')) + versionParser = flag "version" ["Print the version number."] () (argUsage ExitSuccess [greeting t]) + +-- Use the program name as a tool name if possible. +getEffectiveArgs :: ToolParser a -> IO [String] +getEffectiveArgs (Annotated tools _) = do + progName <- getProgName + args <- getArgs + if progName `elem` map toolProgName tools + then return (progName:args) + else return args + +parseCommandLine :: Tool -> ToolParser a -> IO a +parseCommandLine t p = do + let p' = versionTool t `mappend` helpTool t p `mappend` p + args <- getEffectiveArgs p' + case runPref (parser p') args of + Left (Mistake err) -> printHelp (ExitFailure 1) (argError t err) + Left (Usage code err) -> printHelp code err + Right x -> x + +---------------------------------------------------------------------- +-- Help screens. + +printHelp :: ExitCode -> [String] -> IO a +printHelp code xs = do + mapM_ (hPutStrLn stderr ) xs + exitWith code + +argError :: Tool -> String -> [String] +argError t err = [ + greeting t, + err ++ ". Try --help." + ] + +usageTool :: Tool -> String -> [String] -> String -> ToolParser a +usageTool t0 flag msg bit = tool (Tool flag' flag' flag' "0") p + where p = Annotated [] (ParParser (printHelp ExitSuccess msg) + (const (Error (Usage (ExitFailure 1) msg')))) + flag' = "--" ++ flag + msg' = [ + greeting t0, + "Didn't expect any arguments after " ++ flag' ++ ".", + "Try " ++ toolProgName t0 ++ " " ++ flag' ++ " if you want " ++ bit ++ " a particular tool." + ] + +versionTool :: Tool -> ToolParser a +versionTool t0 = usageTool t0 "version" [greeting t0] "the version of" + +helpTool :: Tool -> ToolParser a -> ToolParser a +helpTool t0 p = usageTool t0 "help" help "help for" + where help = concat [ + [greeting t0], + usage t0 " ", + [" can be any of the following:"], + concat [ justify (toolProgName t) [toolHelp t] | t <- descr p ], + ["", "Use " ++ toolProgName t0 ++ " --help for help on a particular tool."] + ] + +help :: Tool -> OptionParser a -> [String] +help t p = concat [ + [greeting t], + usage t "", + ["