packages feed

jukebox 0.4.5 → 0.5

raw patch · 9 files changed

+141/−110 lines, 9 files

Files

jukebox.cabal view
@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.4.5+Version: 0.5 Cabal-version: >= 1.10 Build-type: Simple Author: Nick Smallbone
src/Jukebox/ExternalProvers/E.hs view
@@ -14,6 +14,7 @@ import Data.Maybe import qualified Data.Map.Strict as Map import Data.Map(Map)+import Data.Symbol  data EFlags = EFlags {   eprover :: String,@@ -62,8 +63,8 @@  extractAnswer :: Symbolic a => a -> String -> Either Answer [Term] extractAnswer prob str = fromMaybe (Left status) (fmap Right answer)-  where varMap = Map.fromList [(show (name x), x) | x <- vars prob]-        funMap = Map.fromList [(show (name x), x) | x <- functions prob]+  where varMap = Map.fromList [(intern (show (name x)), x) | x <- vars prob]+        funMap = Map.fromList [(intern (show (name x)), x) | x <- functions prob]         result = lines str         status = head $           [Sat Satisfiable Nothing | "# SZS status Satisfiable" <- result] ++@@ -97,5 +98,5 @@         terms =           bracks (term `sepBy1` punct Comma)           <|> return []-        lookup :: Ord a => Map String a -> String -> a+        lookup :: Map Symbol a -> Symbol -> a         lookup m x = Map.findWithDefault (error "runE: result from E mentions free names") x m
src/Jukebox/Name.hs view
@@ -14,7 +14,7 @@  data Name =     Fixed !FixedName (Maybe String)-  | Unique {-# UNPACK #-} !Int64 String (Maybe String) Renamer+  | Unique {-# UNPACK #-} !Int64 {-# UNPACK #-} !Symbol (Maybe String) Renamer   | Variant !Name ![Name] Renamer  data FixedName =@@ -32,7 +32,7 @@ base x =   case name x of     Fixed x _ -> show x-    Unique _ xs _ _ -> xs+    Unique _ xs _ _ -> unintern xs     Variant x _ _ -> base x  label :: Named a => a -> Maybe String@@ -101,7 +101,7 @@       Nothing -> ""       Just l -> "[" ++ l ++ "]"     where-      Renaming _ ys = f xs 0+      Renaming _ ys = f (unintern xs) 0   show (Variant x xs _) =     "variant(" ++ show x ++       concat [", " ++ show x | x <- xs] ++ ")"@@ -110,8 +110,11 @@   name :: a -> Name  instance Named [Char] where-  name x = Fixed (Basic (intern x)) Nothing+  name x = name (intern x) +instance Named Symbol where+  name x = Fixed (Basic x) Nothing+ instance Named Integer where   name n = name ("n" ++ show n) @@ -168,4 +171,4 @@   let idx' = idx+1   when (idx' < 0) $ error "Name.newName: too many names"   put $! idx'-  return $! Unique idx' (base x) (label x) (renamer x)+  return $! Unique idx' (intern (base x)) (label x) (renamer x)
src/Jukebox/Options.hs view
@@ -18,6 +18,7 @@ import Data.Monoid #endif import Data.Semigroup(Semigroup(..))+import Control.Monad  ---------------------------------------------------------------------- -- A parser of some kind annotated with a help text of some kind@@ -158,7 +159,7 @@ -- it doesn't matter what order we write the options in, -- and because f and x might understand the same flags. data ParParser a = ParParser-  { val :: IO a, -- impure so we can put system information in our options records+  { val :: Either Error (IO a), -- impure so we can put system information in our options records     peek :: [String] -> ParseResult a }  data ParseResult a@@ -177,9 +178,9 @@   fmap f x = pure f <*> x  instance Applicative ParParser where-  pure x = ParParser (return x) (const (pure x))+  pure x = ParParser (Right (return x)) (const (pure x))   ParParser v p <*> ParParser v' p' =-    ParParser (v <*> v') (\xs -> p xs <*> p' xs)+    ParParser (liftM2 (<*>) v v') (\xs -> p xs <*> p' xs)  instance Functor ParseResult where   fmap f x = pure f <*> x@@ -196,15 +197,15 @@   No f <*> No x = No (f <*> x)  runPar :: ParParser a -> [String] -> Either Error (IO a)-runPar p [] = Right (val p)+runPar p [] = 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 -await :: (String -> Bool) -> a -> (String -> [String] -> ParseResult a) -> ParParser a-await p def par = ParParser (return def) f+await :: (String -> Bool) -> Either Error a -> (String -> [String] -> ParseResult a) -> ParParser a+await 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@@ -228,14 +229,14 @@   -- The argument parser is given the option name.   a -> ArgParser (String -> a) -> OptionParser a primFlag name help p combine def (Annotated desc (SeqParser args f)) =-  Annotated [desc'] (await p def (g Right))+  Annotated [desc'] (await p (Right def) (g Right))   where desc' = Flag name "General options" NormalMode help (unwords desc)         g comb x xs =           case f xs >>= comb . ($ x) of             Left (Mistake err) -> Error (Mistake ("Error in option --" ++ name ++ ": " ++ err))             Left (Usage code err) -> Error (Usage code err)             Right y ->-              Yes args (await p y (g (combine y)))+              Yes args (await p (Right y) (g (combine y)))  ---------------------------------------------------------------------- -- Combinators for building OptionParsers.@@ -267,15 +268,19 @@  -- A parser that reads all file names from the command line. filenames :: OptionParser [String]-filenames = Annotated [] (from [])-  where from xs = await p xs (f xs)-        p x = not ("-" `isPrefixOf` x) || x == "-"-        f xs y _ = Yes 0 (from (xs ++ [y]))+filenames = Annotated [] (await p (Left err) (f []))+  where p x = not ("-" `isPrefixOf` x) || x == "-"+        f xs y _ = Yes 0 (let ys = xs ++ [y] in await p (Right ys) (f ys)) +        err =+          Usage (ExitFailure 1)+            ["No input files specified! Try --help.",+             "You can use \"-\" to read from standard input."]+ -- Take a value from the environment. io :: IO a -> OptionParser a io m = Annotated [] p-  where p = ParParser m (const (No p))+  where p = ParParser (Right m) (const (No p))  -- Change the group associated with a set of flags. inGroup :: String -> OptionParser a -> OptionParser a
src/Jukebox/TPTP/Lexer.x view
@@ -3,12 +3,13 @@ -- Roughly taken from the TPTP syntax reference { {-# OPTIONS_GHC -O2 -fno-warn-deprecated-flags #-}-{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE BangPatterns, OverloadedStrings #-} module Jukebox.TPTP.Lexer(   scan,   Pos(..),   Token(..),   Punct(..),+  showPunct,   Defined(..),   Keyword(..),   TokenStream(..),@@ -18,6 +19,7 @@ import Data.Char import Data.Ratio import Codec.Binary.UTF8.String+import Data.Symbol }  $alpha = [a-zA-Z0-9_]@@ -26,6 +28,7 @@ @dquoted = ($printable # [\\\"]) | \\ $printable @pnum = [1-9][0-9]* @num  = 0 | @pnum+@operator = [^\%\(\)\[\]\,\&\|\~\?\!\$'"a-zA-Z0-9_$white]  tokens :- -- Comments and whitespace@@ -71,11 +74,11 @@ -- Atoms with funny quoted names (here we diverge from the official -- syntax, which only allows the escape sequences \\ and \' in quoted -- atoms: we allow \ to be followed by any printable character)-"'"  @quoted+ "'" { Atom Normal . unquote }+"'"  @quoted+ "'" { Atom Normal . copy . unquote } -- Vars are easy :) [A-Z][$alpha]* { Var . copy } -- Distinct objects, which are double-quoted-\" @dquoted+  \" { DistinctObject . unquote }+\" @dquoted+  \" { DistinctObject . copy . unquote } -- Numbers [\+\-]? @num/($anything # $alpha) { Number . read } [\+\-]? @num\/@pnum { Rational . readRational }@@ -91,17 +94,14 @@ ":-" { p LetTerm } -- Operators (TFF) ":" { p Colon }    "*"   { p Times }   "+"  { p Plus }     ">"  { p FunArrow }--- Operators (THF)-"^"  { p Lambda } "@" { p Apply }  "!!" { p ForAllLam }  "??"  { p ExistsLam }-"@+" { p Some }   "@-" { p The }   "<<" { p Subtype }    "-->" { p SequentArrow }-"!>" { p DependentProduct }        "?*" { p DependentSum }+@operator+ { \s -> p (Other (copy s)) s }  { data Pos = Pos {-# UNPACK #-} !Word {-# UNPACK #-} !Word deriving Show-data Token = Atom { keyword :: !Keyword, tokenName :: !String }+data Token = Atom { keyword :: !Keyword, tokenName :: {-# UNPACK #-} !Symbol }            | Defined { defined :: !Defined  }-           | Var { tokenName :: !String }-           | DistinctObject { tokenName :: !String }+           | Var { tokenName :: {-# UNPACK #-} !Symbol }+           | DistinctObject { tokenName :: {-# UNPACK #-} !Symbol }            | Number { value :: !Integer }            | Rational { ratValue :: !Rational }            | Real { ratValue :: !Rational }@@ -147,30 +147,28 @@            | Or | And | Not | Iff | Implies | Follows | Xor | Nor | Nand            | Eq | Neq | ForAll | Exists | Let | LetTerm -- FOF            | Colon | Times | Plus | FunArrow -- TFF-           | Lambda | Apply | ForAllLam | ExistsLam-           | DependentProduct | DependentSum | Some | The-           | Subtype | SequentArrow -- THF+           | Other {-# UNPACK #-} !Symbol -- user-defined              deriving (Eq, Ord) +showPunct :: Punct -> Symbol+showPunct x =+  case x of {+    LParen -> "("; RParen -> ")"; LBrack -> "["; RBrack -> "]";+    Comma -> ","; Dot -> "."; Or -> "|"; And -> "&"; Not -> "~";+    Iff -> "<=>"; Implies -> "=>"; Follows -> "<="; Xor -> "<~>";+    Nor -> "~|"; Nand -> "~&"; Eq -> "="; Neq -> "!="; ForAll -> "!";+    Exists -> "?"; Let -> ":="; Colon -> ":"; Times -> "*"; Plus -> "+";+    FunArrow -> ">"; LetTerm -> ":-"; Other x -> x }+ instance Show Punct where-  show x =-    case x of {-      LParen -> "("; RParen -> ")"; LBrack -> "["; RBrack -> "]";-      Comma -> ","; Dot -> "."; Or -> "|"; And -> "&"; Not -> "~";-      Iff -> "<=>"; Implies -> "=>"; Follows -> "<="; Xor -> "<~>";-      Nor -> "~|"; Nand -> "~&"; Eq -> "="; Neq -> "!="; ForAll -> "!";-      Exists -> "?"; Let -> ":="; Colon -> ":"; Times -> "*"; Plus -> "+";-      FunArrow -> ">"; Lambda -> "^"; Apply -> "@"; ForAllLam -> "!!";-      ExistsLam -> "??"; Some -> "@+"; The -> "@-"; Subtype -> "<<";-      SequentArrow -> "-->"; DependentProduct -> "!>"; DependentSum -> "?*";-      LetTerm -> ":-" }+  show = unintern . showPunct  p x = const (Punct x) k x = Atom x . copy d x = const (Defined x) -copy :: String -> String-copy = id+copy :: String -> Symbol+copy = intern  unquote :: String -> String unquote (_:x)
src/Jukebox/TPTP/Parse/Core.hs view
@@ -20,7 +20,7 @@  import Jukebox.TPTP.Lexer hiding   (Pos, Error, Include, Var, Type, Not, ForAll,-   Exists, And, Or, Type, Apply, Implies, Follows, Xor, Nand, Nor,+   Exists, And, Or, Type, Implies, Follows, Xor, Nand, Nor,    Rational, Real, NegatedConjecture, Question,    Axiom, Hypothesis, Definition, Assumption, Lemma, Theorem, NegatedConjecture,    Conjecture, Question,@@ -35,9 +35,9 @@ data ParseState =   MkState (Maybe String)           -- filename           ![Input Form]            -- problem being constructed, inputs are in reverse order-          !(Map String Type)       -- types in scope-          !(Map String [Function]) -- functions in scope-          !(Map String Variable)   -- variables in scope, for CNF+          !(Map Symbol Type)       -- types in scope+          !(Map Symbol [Function]) -- functions in scope+          !(Map Symbol Variable)   -- variables in scope, for CNF           !Int64                   -- unique supply type Parser = Parsec ParsecState type ParsecState = UserState ParseState TokenStream@@ -49,9 +49,9 @@ initialState :: Maybe String -> ParseState initialState mfile =   initialStateFrom mfile []-    (Map.fromList [(show (name ty), ty) | ty <- [intType, ratType, realType]])+    (Map.fromList [(intern (show (name ty)), ty) | ty <- [intType, ratType, realType]])     (Map.fromList-       [ (fun,+       [ (intern fun,           [Fixed (Overloaded (intern fun) (intern (show (name kind)))) Nothing ::: ty           | (kind, ty) <- tys ])        | (fun, tys) <- funs ])@@ -76,7 +76,7 @@        fun ["$to_rat"]  (\ty -> FunType [ty] ratType) ++        fun ["$to_real"] (\ty -> FunType [ty] realType) -initialStateFrom :: Maybe String -> [Name] -> Map String Type -> Map String [Function] -> ParseState+initialStateFrom :: Maybe String -> [Name] -> Map Symbol Type -> Map Symbol [Function] -> ParseState initialStateFrom mfile xs tys fs = MkState mfile [] tys fs Map.empty n   where     n = maximum (0:[succ m | Unique m _ _ _ <- xs])@@ -174,6 +174,16 @@         p' _ = False {-# INLINE punct #-} punct k = punct' (== k) <?> "'" ++ show k ++ "'"+{-# INLINE operator #-}+operator = punct' p <?> "operator"+  where+    p Dot = True+    p Colon = True+    p Times = True+    p Plus = True+    p FunArrow = True+    p (Other _) = True+    p _ = False {-# INLINE defined' #-} defined' p = fmap L.defined (satisfy p')   where p' Defined { L.defined = d } = p d@@ -277,7 +287,7 @@  -- A formula name. tag :: Parser Tag-tag = atom <|> fmap show number <?> "clause name"+tag = fmap unintern atom <|> fmap show number <?> "clause name"  -- An include declaration. include :: Parser IncludeStatement@@ -287,7 +297,7 @@     name <- atom <?> "quoted filename"     clauses <- do { punct Comma                   ; fmap Just (bracks (sepBy1 tag (punct Comma))) } <|> return Nothing-    return (Include name clauses)+    return (Include (unintern name) clauses)   punct Dot   return res @@ -298,12 +308,12 @@   MkState mfile p t f v n <- getState   putState (MkState mfile (input:p) t f v n)   -newFunction :: String -> FunType -> Parser Function+newFunction :: Symbol -> FunType -> Parser Function newFunction name ty = do   fs <- lookupFunction ty name   case [ f | f <- fs, rhs f == ty ] of     [] ->-      fatalError $ "Constant " ++ name +++      fatalError $ "Constant " ++ unintern name ++                    " was declared to have type " ++ prettyShow ty ++                    " but already has type " ++ showTypes (map rhs fs)     (f:_) -> return f@@ -312,7 +322,7 @@ showTypes = intercalate " and " . map prettyShow  {-# INLINE applyFunction #-}-applyFunction :: String -> [Term] -> Type -> Parser Term+applyFunction :: Symbol -> [Term] -> Type -> Parser Term applyFunction name args res = do   fs <- lookupFunction (FunType (replicate (length args) indType) res) name   case [ f | f <- fs, funArgs f == map typ args ] of@@ -336,7 +346,7 @@                    " of type " ++ intercalate ", " (map (prettyShow . typ) args')  {-# INLINE lookupType #-}-lookupType :: String -> Parser Type+lookupType :: Symbol -> Parser Type lookupType xs = do   MkState mfile p t f v n <- getState   case Map.lookup xs t of@@ -347,7 +357,7 @@     Just ty -> return ty  {-# INLINE lookupFunction #-}-lookupFunction :: FunType -> String -> Parser [Name ::: FunType]+lookupFunction :: FunType -> Symbol -> Parser [Name ::: FunType] lookupFunction def x = do   MkState mfile p t f v n <- getState   case Map.lookup x f of@@ -376,14 +386,14 @@ -- A thing is either a term or a formula, or a literal that we don't know -- if it should be a term or a formula. Instead of a separate formula-parser -- and term-parser we have a combined thing-parser.-data Thing = Apply !String ![Term]+data Thing = Apply !Symbol ![Term]            | Term !Term            | Formula !Form  instance Show Thing where-  show (Apply f []) = f+  show (Apply f []) = unintern f   show (Apply f args) =-    f +++    unintern f ++       case args of         [] -> ""         args -> prettyShow args@@ -395,7 +405,7 @@ -- the error messages are better). For that reason, our parser is -- parametrised on the type of thing you want to parse. We have two -- main parsers:---   * 'term' parses an atomic expression+--   * 'term' parses a term or predicate --   * 'formula' parses an arbitrary expression -- You can instantiate 'term' for Term, Form or Thing; in each case -- you get an appropriate parser. You can instantiate 'formula' for@@ -407,9 +417,11 @@   -- Convert from a Thing.   fromThing :: Thing -> Parser a   -- Parse a variable occurrence as a term on its own, if that's allowed.-  var :: Mode -> Map String Variable -> Parser a+  var :: Mode -> Map Symbol Variable -> Parser a+  -- Parse the input as a formula, if that's allowed.+  parseFormula :: Parser Form -> Parser a   -- A parser for this type.-  parser :: Mode -> Map String Variable -> Parser a+  parser :: Mode -> Map Symbol Variable -> Parser a  data Mode = Typed | Untyped | NoQuantification @@ -420,6 +432,7 @@   fromThing (Formula f) = return f   -- A variable itself is not a valid formula.   var _ _ = mzero+  parseFormula = id   parser = formula  instance TermLike Term where@@ -427,6 +440,7 @@   fromThing (Apply x xs) = applyFunction x xs indType   fromThing (Term t) = return t   fromThing (Formula _) = mzero+  parseFormula _ = mzero   parser = term    {-# INLINE var #-}@@ -443,25 +457,18 @@     x <- variable     case Map.lookup x ctx of       Just v -> return (Var v)-      Nothing -> fatalError $ "unbound variable " ++ x+      Nothing -> fatalError $ "unbound variable " ++ unintern x  instance TermLike Thing where   fromThing = return   var mode ctx = fmap Term (var mode ctx)+  parseFormula = fmap Formula   parser = formula --- Types that can represent formulae. These are the types on which--- you can use 'formula'.-class TermLike a => FormulaLike a where-  fromFormula :: Form -> a--instance FormulaLike Form where fromFormula = id-instance FormulaLike Thing where fromFormula = Formula- -- An atomic expression.-{-# INLINEABLE term #-}-term :: TermLike a => Mode -> Map String Variable -> Parser a-term mode ctx = function <|> var mode ctx <|> num <|> parens (parser mode ctx)+{-# INLINEABLE atomic #-}+atomic :: TermLike a => Mode -> Map Symbol Variable -> Parser a+atomic mode ctx = function <|> var mode ctx <|> num <|> parens (parser mode ctx)   where     {-# INLINE function #-}     function = do@@ -491,18 +498,36 @@     constant x ty =       fromThing (Term ((Fixed x Nothing ::: FunType [] ty) :@: [])) +unary :: TermLike a => Mode -> Map Symbol Variable -> Parser a+unary mode ctx =+  atomic mode ctx <|> do+    Punct p <- operator+    arg <- atomic mode ctx :: Parser Term+    fromThing (Apply (showPunct p) [arg])++term :: TermLike a => Mode -> Map Symbol Variable -> Parser a+term mode ctx = do+  t <- unary mode ctx :: Parser Thing+  let+    binop = do+      Punct p <- operator+      lhs <- fromThing t :: Parser Term+      rhs <- unary mode ctx :: Parser Term+      fromThing (Apply (showPunct p) [lhs, rhs])+  binop <|> fromThing t+ literal, unitary, quantified, formula ::-  FormulaLike a => Mode -> Map String Variable -> Parser a+  TermLike a => Mode -> Map Symbol Variable -> Parser a {-# INLINE literal #-} literal mode ctx = true <|> false <|> binary <?> "literal"   where {-# INLINE true #-}-        true = do { defined DTrue; return (fromFormula (And [])) }+        true = parseFormula $ do { defined DTrue; return (And []) }         {-# INLINE false #-}-        false = do { defined DFalse; return (fromFormula (Or [])) }+        false = parseFormula $ do { defined DFalse; return (Or []) }         binary = do           x <- term mode ctx :: Parser Thing           let {-# INLINE f #-}-              f p sign = do+              f p sign = parseFormula $ do                punct p                lhs <- fromThing x :: Parser Term                rhs <- term mode ctx :: Parser Term@@ -514,25 +539,25 @@                when (typ lhs == O) $                  fatalError $ "Type error in equality '" ++ prettyShow (prettyNames form) ++                  "': can't use equality on predicate (use <=> or <~> instead)"-               return (fromFormula form)+               return form           f Eq Pos <|> f Neq Neg <|> fromThing x  {-# INLINEABLE unitary #-} unitary mode ctx = negation <|> quantified mode ctx <|> literal mode ctx   where {-# INLINE negation #-}-        negation = do+        negation = parseFormula $ do           punct L.Not-          fmap (fromFormula . Not) (unitary mode ctx :: Parser Form)+          fmap Not $ unitary mode ctx  {-# INLINE quantified #-}-quantified mode ctx = do+quantified mode ctx = parseFormula $ do   q <- (punct L.ForAll >> return ForAll) <|>        (punct L.Exists >> return Exists)   vars <- bracks (sepBy1 (binder mode) (punct Comma))-  let ctx' = foldl' (\m v -> Map.insert (Name.base (Name.name v)) v m) ctx vars+  let ctx' = foldl' (\m v -> Map.insert (intern (Name.base (Name.name v))) v m) ctx vars   punct Colon   rest <- unitary mode ctx' :: Parser Form-  return (fromFormula (q (Bind (Set.fromList vars) rest)))+  return (q (Bind (Set.fromList vars) rest))  -- A general formula. {-# INLINEABLE formula #-}@@ -540,11 +565,11 @@   x <- unitary mode ctx :: Parser Thing   let binop op t u = op [t, u]       {-# INLINE connective #-}-      connective p op = do+      connective p op = parseFormula $ do         punct p         lhs <- fromThing x         rhs <- formula mode ctx :: Parser Form-        return (fromFormula (op lhs rhs))+        return (op lhs rhs)   connective L.And (binop And) <|> connective L.Or (binop Or) <|>    connective Iff Equiv <|>    connective L.Implies (Connective Implies) <|>
src/Jukebox/TPTP/ParseSnippet.hs view
@@ -1,6 +1,6 @@ -- Parse little bits of TPTP, e.g. a prelude for a particular tool. -{-# LANGUAGE CPP #-}+{-# LANGUAGE CPP, OverloadedStrings #-} module Jukebox.TPTP.ParseSnippet where  import Jukebox.TPTP.Parse.Core as TPTP.Parse.Core@@ -13,41 +13,43 @@ #if __GLASGOW_HASKELL__ < 710 import Control.Applicative #endif+import Data.Symbol  tff, cnf :: [(String, Type)] -> [(String, Function)] -> String -> Form tff = form TPTP.Parse.Core.tff cnf = form TPTP.Parse.Core.cnf  form :: Symbolic a => Parser a -> [(String, Type)] -> [(String, Function)] -> String -> a-form parser types funs0 str =+form parser types0 funs0 str =   case run_ (parser <* eof)-            (UserState (MkState Nothing [] (Map.delete "$i" (Map.fromList types)) (Map.fromList funs) Map.empty 0) (scan str)) of+            (UserState (MkState Nothing [] (Map.delete "$i" types) funs Map.empty 0) (scan str)) of     Ok (UserState (MkState _ _ types' funs' _ _) (At _ (Cons Eof _))) res-      | Map.insert "$i" indType (Map.fromList types) /=+      | Map.insert "$i" indType types /=         Map.insert "$i" indType types' ->         error $ "ParseSnippet: type implicitly defined: " ++-                show (map snd (Map.toList types' \\ types))-      | Map.fromList funs /= funs' ->+                show (map snd (Map.toList types' \\ Map.toList types))+      | funs /= funs' ->         error $ "ParseSnippet: function implicitly defined: " ++-                show (map snd (Map.toList funs' \\ funs))+                show (map snd (Map.toList funs' \\ Map.toList funs))       | otherwise -> mapType elimI res     Ok{} -> error "ParseSnippet: lexical error"     TPTP.Parsec.Error _ msg -> error $ "ParseSnippet: parse error: " ++ msg     Expected _ exp -> error $ "ParseSnippet: parse error: expected " ++ show exp    where-    funs = map (mapFunType introI) funs0+    funs = Map.mapKeys intern $ Map.fromList $ map (mapFunType introI) funs0+    types = Map.mapKeys intern $ Map.fromList types0      mapFunType f (xs, name ::: FunType args res) =       (xs, [name ::: FunType (map f args) (f res)])      elimI =-      case lookup "$i" types of+      case Map.lookup "$i" types of         Nothing -> id         Just i ->           \ty -> if ty == indType then i else ty     introI =-      case lookup "$i" types of+      case Map.lookup "$i" types of         Nothing -> id         Just i ->           \ty -> if ty == i then indType else ty
src/Jukebox/TPTP/Print.hs view
@@ -18,6 +18,7 @@ import Jukebox.Utils import Text.PrettyPrint.HughesPJClass import Control.Monad.Trans.State.Strict+import Data.Symbol  pPrintClauses :: Problem Clause -> Doc pPrintClauses prob0@@ -204,10 +205,10 @@   pPrint = text . show  instance Show L.Token where-  show L.Atom{L.tokenName = x} = escapeAtom x+  show L.Atom{L.tokenName = x} = escapeAtom (unintern x)   show L.Defined{L.defined = x} = show x-  show L.Var{L.tokenName = x} = x-  show L.DistinctObject{L.tokenName = x} = quote '"' x+  show L.Var{L.tokenName = x} = unintern x+  show L.DistinctObject{L.tokenName = x} = quote '"' (unintern x)   show L.Number{L.value = x} = show x   show L.Punct{L.kind = x} = show x   show L.Eof = "end of file"@@ -340,7 +341,7 @@     add1 (Fixed xs _) (scope, used) =       (scope, Set.insert (show xs) used)     add1 x@(Unique _ base _ f) (scope, used) =-      addWith base f x (scope, used)+      addWith (unintern base) f x (scope, used)     add1 x@(Variant y _ f) (scope, used) =       addWith (base y) f x (scope, used)
src/Jukebox/Toolbox.hs view
@@ -93,10 +93,6 @@ forAllFilesBox = forAllFiles <$> filenames  forAllFiles :: [FilePath] -> (FilePath -> IO ()) -> IO ()-forAllFiles [] _ = do-  hPutStrLn stderr "No input files specified! Try --help."-  hPutStrLn stderr "You can use \"-\" to read from standard input."-  exitWith (ExitFailure 1) forAllFiles xs f = mapM_ f xs  ----------------------------------------------------------------------