diff --git a/Jukebox/Clausify.hs b/Jukebox/Clausify.hs deleted file mode 100644 --- a/Jukebox/Clausify.hs +++ /dev/null @@ -1,446 +0,0 @@ -{-# 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 deleted file mode 100644 --- a/Jukebox/Form.hs +++ /dev/null @@ -1,716 +0,0 @@ --- 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 deleted file mode 100644 --- a/Jukebox/GuessModel.hs +++ /dev/null @@ -1,121 +0,0 @@ -{-# 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 deleted file mode 100644 --- a/Jukebox/HighSat.hs +++ /dev/null @@ -1,114 +0,0 @@ -{-# 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) -import Control.Applicative - -newtype Sat1 a b = Sat1 { runSat1_ :: ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b } deriving (Functor, Applicative, Monad, MonadIO) -newtype Sat a b c = Sat { runSat_ :: ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c } deriving (Functor, Applicative, 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 deleted file mode 100644 --- a/Jukebox/InferTypes.hs +++ /dev/null @@ -1,82 +0,0 @@ -{-# 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 deleted file mode 100644 --- a/Jukebox/Map.hs +++ /dev/null @@ -1,28 +0,0 @@ -{-# 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 deleted file mode 100644 --- a/Jukebox/Monotonox/Monotonicity.hs +++ /dev/null @@ -1,82 +0,0 @@ -{-# 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 deleted file mode 100644 --- a/Jukebox/Monotonox/ToFOF.hs +++ /dev/null @@ -1,191 +0,0 @@ -{-# 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 deleted file mode 100644 --- a/Jukebox/Name.hs +++ /dev/null @@ -1,153 +0,0 @@ -{-# 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 -import Control.Applicative - -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, Applicative, 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 deleted file mode 100644 --- a/Jukebox/NameMap.hs +++ /dev/null @@ -1,46 +0,0 @@ -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 deleted file mode 100644 --- a/Jukebox/Options.hs +++ /dev/null @@ -1,358 +0,0 @@ -{-# 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 <- - case tools of - [tool] -> return (toolProgName tool) - _ -> 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' = - case p of - Annotated [_] _ -> 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 "", - ["