{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, CPP, GeneralizedNewtypeDeriving, TypeFamilies, RecordWildCards, FlexibleContexts, UndecidableInstances, NondecreasingIndentation #-} #include "errors.h" #if __GLASGOW_HASKELL__ < 710 import Control.Applicative #endif import Control.Monad import Control.Monad.Trans.State.Strict import Data.Char import Data.Either import Twee hiding (info) import Twee.Base hiding (char, lookup, (<>)) import Twee.Rule import Twee.Utils import Twee.Queue import Data.Ord import qualified Twee.Indexes as Indexes import qualified Data.Map.Strict as Map import qualified Twee.KBO as KBO import qualified Twee.LPO as LPO import qualified Data.Set as Set import Data.Reflection import qualified Data.IntMap as IntMap import Data.IntMap(IntMap) import Data.List.Split import Data.List import Data.Maybe import Jukebox.Options import Jukebox.Toolbox import Jukebox.Name import qualified Jukebox.Form as Jukebox import Jukebox.Form hiding ((:=:), Var, Symbolic(..), Term) import qualified Twee.Label as Label parseInitialState :: OptionParser (Twee f) parseInitialState = go <$> maxSize <*> general <*> groundJoin <*> conn <*> set <*> setGoals <*> tracing <*> moreTracing <*> lweight <*> rweight <*> splits <*> cpSetSize <*> mixFIFO <*> mixPrio <*> skipComposite <*> interreduce <*> unsafeInterreduce <*> cancel <*> cancelSize <*> cancelConsts <*> atomicCancellation where go maxSize general groundJoin conn set setGoals tracing moreTracing lweight rweight splits cpSetSize mixFIFO mixPrio skipComposite interreduce unsafeInterreduce cancel cancelSize cancelConsts atomicCancellation = (initialState mixFIFO mixPrio) { maxSize = maxSize, cpSplits = splits, minimumCPSetSize = cpSetSize, useGeneralSuperpositions = general, useGroundJoining = groundJoin, useConnectedness = conn, useSetJoining = set, useSetJoiningForGoals = setGoals, useCancellation = cancel, maxCancellationSize = cancelSize, atomicCancellation = atomicCancellation, unifyConstantsInCancellation = cancelConsts, useInterreduction = interreduce, useUnsafeInterreduction = unsafeInterreduce, skipCompositeSuperpositions = skipComposite, tracing = tracing, moreTracing = moreTracing, lhsWeight = lweight, rhsWeight = rweight } maxSize = flag "max-size" ["Maximum critical pair size"] Nothing (Just <$> argNum) general = not <$> bool "no-general-superpositions" ["Disable considering only general superpositions"] groundJoin = not <$> bool "no-ground-join" ["Disable ground joinability testing"] conn = not <$> bool "no-connectedness" ["Disable connectedness testing"] set = bool "set-join" ["Join by computing set of normal forms"] setGoals = not <$> bool "no-set-join-goals" ["Disable joining goals by computing set of normal forms"] tracing = not <$> bool "no-tracing" ["Disable tracing output"] moreTracing = bool "more-tracing" ["Produce even more tracing output"] lweight = flag "lhs-weight" ["Weight given to LHS of critical pair (default 2)"] 2 argNum rweight = flag "rhs-weight" ["Weight given to RHS of critical pair (default 1)"] 1 argNum splits = flag "split" ["Split CP sets into this many pieces on selection (default 20)"] 20 argNum cpSetSize = flag "cp-set-minimum" ["Decay CP sets into single CPs when they get this small (default 20)"] 20 argNum mixFIFO = flag "mix-fifo" ["Take this many CPs at a time from FIFO (default 0)"] 0 argNum mixPrio = flag "mix-prio" ["Take this many CPs at a time from priority queue (default 10)"] 10 argNum interreduce = bool "interreduce" ["Enable interreduction of left hand sides"] unsafeInterreduce = not <$> bool "safe-interreduce" ["Disable some incomplete interreductions"] cancel = not <$> bool "no-cancellation" ["Disable cancellation"] cancelSize = flag "max-cancellation-size" ["Maximum size of cancellation laws"] Nothing (Just <$> argNum) cancelConsts = bool "unify-consts-in-cancellation" ["Allow unification with a constant in cancellation"] skipComposite = not <$> bool "composite-superpositions" ["Generate composite superpositions"] atomicCancellation = not <$> bool "compound-cancellation" ["Allow cancellation laws to have non-atomic RHS"] data Order = KBO | LPO parseOrder :: OptionParser Order parseOrder = f <$> bool "lpo" ["Use lexicographic path ordering instead of KBO"] where f False = KBO f True = LPO parsePrecedence :: OptionParser [String] parsePrecedence = fmap (splitOn ",") (flag "precedence" ["List of functions in descending order of precedence"] [] (arg "" "expected a function name" Just)) data Constant = Constant { conIndex :: Int, conArity :: Int, conSize :: Int, conName :: String } | Builtin Builtin data Builtin = CFalse | CTrue | CEquals deriving (Eq, Ord) instance Eq Constant where x == y = x `compare` y == EQ instance Ord Constant where compare Constant{conIndex = x} Constant{conIndex = y} = compare x y compare Constant{} Builtin{} = LT compare Builtin{} Constant{} = GT compare (Builtin x) (Builtin y) = compare x y instance Sized Constant where size Constant{conSize = n} = fromIntegral n size Builtin{} = 0 instance Arity Constant where arity Constant{conSize = n} = n arity (Builtin CEquals) = 2 arity (Builtin _) = 0 instance Pretty Constant where pPrint Constant{conName = name} = text name pPrint (Builtin CEquals) = text "$equals" pPrint (Builtin CTrue) = text "$true" pPrint (Builtin CFalse) = text "$false" instance PrettyTerm Constant where termStyle con@Constant{} | not (any isAlphaNum (conName con)) = case conArity con of 1 -> prefix 2 -> infixStyle 5 _ -> uncurried termStyle _ = uncurried instance Given (IntMap Constant) => Numbered Constant where fromInt 0 = Builtin CFalse fromInt 1 = Builtin CTrue fromInt 2 = Builtin CEquals fromInt n = IntMap.findWithDefault __ (n-3) given toInt Constant{conIndex = n} = n+3 toInt (Builtin CFalse) = 0 toInt (Builtin CTrue) = 1 toInt (Builtin CEquals) = 2 instance (Given Order, Given (IntMap Constant)) => Ordered (Extended Constant) where lessEq = case given of KBO -> KBO.lessEq LPO -> LPO.lessEq lessIn = case given of KBO -> KBO.lessIn LPO -> LPO.lessIn instance Label.Labelled Jukebox.Function where cache = functionCache {-# NOINLINE functionCache #-} functionCache :: Label.Cache Jukebox.Function functionCache = Label.mkCache instance Numbered Jukebox.Function where fromInt n = fromMaybe __ (Label.find n) toInt = Label.label toTwee :: Problem Clause -> ([Equation Jukebox.Function], [Term Jukebox.Function]) toTwee prob = (lefts eqs, goals) where eq Input{what = Clause (Bind _ [Pos (t Jukebox.:=: u)])} = Left (tm t :=: tm u) eq Input{what = Clause (Bind _ [Neg (t Jukebox.:=: u)])} = Right (tm t :=: tm u) eq _ = ERROR("Problem is not unit equality") eqs = map eq prob goals = case rights eqs of [] -> [] [t :=: u] -> [t, u] _ -> ERROR("Problem is not unit equality") tm (Jukebox.Var (Unique x _ _ ::: _)) = build (var (MkVar (fromIntegral x))) tm (f :@: ts) = app f (map tm ts) addNarrowing :: Given (IntMap Constant) => ([Equation (Extended Constant)], [Term (Extended Constant)]) -> ([Equation (Extended Constant)], [Term (Extended Constant)]) addNarrowing (axioms, goals) | length goals < 2 = (axioms, [app false [], app true []]) where false = Function (Builtin CFalse) true = Function (Builtin CTrue) addNarrowing (axioms, goals) | length goals >= 2 && all isGround goals = (axioms, goals) addNarrowing (axioms, [t, u]) | otherwise = (axioms ++ equalities, [app false [], app true []]) where false = Function (Builtin CFalse) true = Function (Builtin CTrue) equals = Function (Builtin CEquals) equalities = [app equals [build (var (MkVar 0)), build (var (MkVar 0))] :=: app true [], app equals [t, u] :=: app false []] addNarrowing _ = ERROR("Don't know how to handle several non-ground goals") runTwee :: Twee (Extended Constant) -> Order -> [String] -> Problem Clause -> IO Answer runTwee state order precedence obligs = do let (axioms0, goals0) = toTwee obligs prec c = (isNothing (elemIndex (base c) precedence), fmap negate (elemIndex (base c) precedence), negate (occ (toFun c) (axioms0, goals0))) fs0 = map fromFun (usort (funs (axioms0, goals0))) fs1 = sortBy (comparing prec) fs0 fs2 = zipWith (\i (c ::: (FunType args _)) -> Constant i (length args) 1 (show c)) [1..] fs1 m = IntMap.fromList [(conIndex f, f) | f <- fs2] m' = Map.fromList (zip fs1 (map Function fs2)) give m $ give order $ do let replace = build . mapFun (toFun . flip (Map.findWithDefault __) m' . fromFun) axioms1 = [replace t :=: replace u | t :=: u <- axioms0] goals1 = map replace goals0 (axioms2, goals2) = addNarrowing (axioms1, goals1) putStrLn "Axioms:" mapM_ prettyPrint axioms2 putStrLn "\nGoals:" mapM_ prettyPrint goals2 putStrLn "\nGo!" let identical xs = not (Set.null (foldr1 Set.intersection xs)) loop = do res <- complete1 goals <- gets goals when (res && (length goals <= 1 || not (identical goals))) loop s = flip execState (addGoals (map Set.singleton goals2) state) $ do mapM_ newEquation axioms2 loop rs = map (critical . modelled . peel) (Indexes.elems (labelledRules s)) putStrLn "\nFinal rules:" mapM_ prettyPrint rs putStrLn "" putStrLn (report s) putStrLn "Normalised goal terms:" forM_ goals2 $ \t -> prettyPrint (Rule Oriented t (result (normalise s t))) return $ case () of _ | identical (goals s) -> Unsatisfiable | isJust (maxSize s) -> NoAnswer GaveUp | otherwise -> Satisfiable main = do let twee = Tool "twee" "twee - the Wonderful Equation Engine" "1" "Proves equations." join . parseCommandLine twee . tool twee $ greetingBox twee =>> allFilesBox <*> (parseProblemBox =>>= toFofBox =>>= clausifyBox =>>= allObligsBox <*> (runTwee <$> parseInitialState <*> parseOrder <*> parsePrecedence))