Clean warnings, drop lexicon from Megalodon export

4 files changed, 75 insertions, 77 deletions

diff --git a/source/Api.hs b/source/Api.hs
index 0e05cbd..2b71de2 100644
--- a/source/Api.hs
+++ b/source/Api.hs
@@ -297,8 +297,8 @@ dumpTask file tptp = liftIO (Text.writeFile file (Tptp.toText tptp))
 
 exportMegalodon :: (MonadUnliftIO io) => FilePath -> io Text
 exportMegalodon file = do
-    (blocks, lexicon) <- gloss file
-    pure (Megalodon.encodeBlocks lexicon blocks)
+    (blocks, _lexicon) <- gloss file
+    pure (Megalodon.encodeBlocks blocks)
 
 
 
diff --git a/source/Meaning.hs b/source/Meaning.hs
index 448ec0c..77144e4 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -246,9 +246,9 @@ glossChain ch = Sem.makeConjunction <$> makeRels (conjuncts (splat ch))
             e1' <- glossExpr e1
             e2' <- glossExpr e2
             case rel of
-                Raw.Relation rel params -> do
+                Raw.Relation rel' params -> do
                     params' <- glossExpr `each` params
-                    pure $ sign' $ Sem.Relation Nowhere rel (params' <> [e1',e2'])
+                    pure $ sign' $ Sem.Relation Nowhere rel' (params' <> [e1',e2'])
                 Raw.RelationExpr e -> do
                             e' <- glossExpr e
                             pure (sign' (Sem.IsElementOf Nowhere (Sem.TermPair Nowhere e1' e2') e'))
@@ -340,10 +340,10 @@ glossAdjL (Raw.AdjL loc pat es) = do
 -- the term representing the subject, hence the parameter 'Sem.Expr'.
 glossAdjR :: Raw.AdjR -> Gloss (Sem.Term -> Sem.Formula)
 glossAdjR = \case
-    Raw.AdjR loc pat [e] | pat == Raw.mkLexicalItem (unsafeReadPhrase "equal to ?") "eq" -> do
+    Raw.AdjR _loc pat [e] | pat == Raw.mkLexicalItem (unsafeReadPhrase "equal to ?") "eq" -> do
         (e', quantify) <- glossTerm e
         pure $ \t -> quantify $ Sem.Equals Nowhere t e'
-    Raw.AdjR loc pat es -> do
+    Raw.AdjR _loc pat es -> do
         (es', quantifies) <- unzip <$> glossTerm `each` es
         let quantify = compose $ reverse quantifies
         pure $ \t -> quantify $ Sem.FormulaAdj Nowhere t pat es'
@@ -396,15 +396,15 @@ glossFun (Raw.Fun loc phrase es) = do
 
 glossTerm :: Raw.Term -> Gloss (Sem.Term, Sem.Formula -> Sem.Formula)
 glossTerm = \case
-    Raw.TermExpr loc e ->
+    Raw.TermExpr _loc e ->
         (, id) <$> glossExpr e
     Raw.TermFun f ->
         glossFun f
-    Raw.TermIota loc x stmt -> do
-        stmt' <- glossStmt stmt
+    Raw.TermIota _loc _x stmt -> do
+        _stmt' <- glossStmt stmt
         _TODO "glossTerm TermIota"
         --pure (Sem.Iota x (abstract1 x stmt'), id)
-    Raw.TermQuantified quantifier loc np -> do
+    Raw.TermQuantified quantifier _loc np -> do
         quantify <- glossQuantifier quantifier
         (mkConstraint, maySuchThat) <- glossNPMaybe np
         v <- freshVar
@@ -416,14 +416,14 @@ glossTerm = \case
 
 glossStmt :: Raw.Stmt -> Gloss Sem.Formula
 glossStmt = \case
-    Raw.StmtFormula loc f -> glossFormula f
+    Raw.StmtFormula _loc f -> glossFormula f
     Raw.StmtNeg loc s -> Sem.Not loc <$> glossStmt s
     Raw.StmtVerbPhrase ts vp -> do
         (ts', quantifies) <- NonEmpty.unzip <$> glossTerm `each` ts
         vp' <- glossVP vp
         let phi = Sem.makeConjunction (vp' <$> toList ts')
         pure (compose quantifies phi)
-    Raw.StmtNoun loc ts np -> do
+    Raw.StmtNoun _loc ts np -> do
         (ts', quantifies) <- NonEmpty.unzip <$> glossTerm `each` ts
         (np', maySuchThat) <- glossNPMaybe np
         let andSuchThat phi = case maySuchThat of
@@ -434,16 +434,16 @@ glossStmt = \case
     Raw.StmtStruct loc t sp -> do
         (t', quantify) <- glossTerm t
         pure (quantify (Sem.TermSymbol loc (Sem.SymbolPredicate (Sem.PredicateNounStruct sp)) [t']))
-    Raw.StmtConnected conn mpos s1 s2 -> glossConnective conn <*> glossStmt s1 <*> glossStmt s2
-    Raw.StmtQuantPhrase loc (Raw.QuantPhrase quantifier np) f -> do
+    Raw.StmtConnected conn _mpos s1 s2 -> glossConnective conn <*> glossStmt s1 <*> glossStmt s2
+    Raw.StmtQuantPhrase _loc (Raw.QuantPhrase quantifier np) f -> do
         (vars, constraints) <- glossNPList np
         f' <- glossStmt f
         quantify <- glossQuantifier quantifier
         pure (quantify vars [constraints] f')
-    Raw.StmtExists loc np -> do
+    Raw.StmtExists _loc np -> do
         (vars, constraints) <- glossNPList np
         pure (Sem.makeExists vars constraints)
-    Raw.SymbolicQuantified loc quant vs bound suchThat have -> do
+    Raw.SymbolicQuantified _loc quant vs bound suchThat have -> do
         quantify <- glossQuantifier quant
         bound' <- glossBound bound
         suchThatConstraints <- maybeToList <$> glossStmt `each` suchThat
@@ -464,10 +464,10 @@ glossBound = \case
                 Positive -> id
                 Negative -> Sem.Not Nowhere
         bound <- case rel of
-            Raw.Relation rel params -> do
+            Raw.Relation rel' params -> do
                 params' <- glossExpr `each` params
                 pure $ \v -> sign' $
-                    Sem.Relation Nowhere rel (params' <> [Sem.TermVar v, term'])
+                    Sem.Relation Nowhere rel' (params' <> [Sem.TermVar v, term'])
             Raw.RelationExpr e -> do
                 e' <- glossExpr e
                 pure $ \v -> sign' $
@@ -552,7 +552,7 @@ glossLemma (Raw.Lemma asms f) = Sem.Lemma <$> glossAsms asms <*> glossStmt f
 glossDefn :: Raw.Defn -> Gloss Sem.Defn
 glossDefn = \case
     Raw.Defn asms h f -> glossDefnHead h <*> glossAsms asms <*> glossStmt f
-    Raw.DefnFun asms (Raw.Fun loc fun vs) _ e -> do
+    Raw.DefnFun asms (Raw.Fun _loc fun vs) _ e -> do
         asms' <- glossAsms asms
         e' <- case e of
             -- TODO improve error handling or make grammar stricter
@@ -568,13 +568,13 @@ glossDefn = \case
 glossDefnHead :: Raw.DefnHead -> Gloss ([Sem.Asm] -> Sem.Formula -> Sem.Defn)
 glossDefnHead = \case
     -- TODO add info from NP.
-    Raw.DefnAdj _mnp v (Raw.Adj loc adj vs) -> do
+    Raw.DefnAdj _mnp v (Raw.Adj _loc adj vs) -> do
         pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateAdj adj) (v :| vs) f
         --mnp' <- glossNPMaybe `each` mnp
         --pure $ case mnp' of
         --    Nothing  -> \asms f -> Sem.DefnPredicate asms (Sem.PredicateAdj adj') (v :| vs) f
         --    Just np' -> \asms f -> Sem.DefnPredicate asms (Sem.PredicateAdj adj') (v :| vs) (Sem.FormulaAnd (np' v) f)
-    Raw.DefnVerb _mnp v (Raw.Verb loc verb vs) ->
+    Raw.DefnVerb _mnp v (Raw.Verb _loc verb vs) ->
         pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateVerb verb) (v :| vs) f
     Raw.DefnNoun v (Raw.Noun noun vs) ->
         pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateNoun noun) (v :| vs) f
@@ -685,9 +685,9 @@ glossCalc = \case
 
 glossSignature :: Raw.Signature -> Gloss Sem.Signature
 glossSignature sig = case sig of
-    Raw.SignatureAdj v (Raw.Adj loc adj vs) ->
+    Raw.SignatureAdj v (Raw.Adj _loc adj vs) ->
         pure $ Sem.SignaturePredicate (Sem.PredicateAdj adj) (v :| vs)
-    Raw.SignatureVerb v (Raw.Verb loc verb vs) ->
+    Raw.SignatureVerb v (Raw.Verb _loc verb vs) ->
         pure $ Sem.SignaturePredicate (Sem.PredicateVerb verb) (v :| vs)
     Raw.SignatureNoun v (Raw.Noun noun vs) ->
         pure $ Sem.SignaturePredicate (Sem.PredicateNoun noun) (v :| vs)
@@ -722,15 +722,15 @@ annotateCarrierFormula lbl = \case
 
 glossAbbreviation :: Raw.Abbreviation -> Gloss Sem.Abbreviation
 glossAbbreviation = \case
-    Raw.AbbreviationAdj x (Raw.Adj loc adj xs) stmt ->
+    Raw.AbbreviationAdj x (Raw.Adj _loc adj xs) stmt ->
         makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateAdj adj)) (x : xs) stmt
-    Raw.AbbreviationVerb x (Raw.Verb loc verb xs) stmt ->
+    Raw.AbbreviationVerb x (Raw.Verb _loc verb xs) stmt ->
         makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateVerb verb)) (x : xs) stmt
     Raw.AbbreviationNoun x (Raw.Noun noun xs) stmt ->
         makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateNoun noun)) (x : xs) stmt
     Raw.AbbreviationRel x rel params y stmt ->
         makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateRelation rel)) (params <> [x, y]) stmt
-    Raw.AbbreviationFun (Raw.Fun loc fun xs) t ->
+    Raw.AbbreviationFun (Raw.Fun _loc fun xs) t ->
         makeAbbrTerm (Sem.SymbolFun fun) xs t
     Raw.AbbreviationEq (Raw.SymbolPattern op xs) e ->
         makeAbbrExpr (Sem.SymbolMixfix op) xs e
diff --git a/source/Megalodon.hs b/source/Megalodon.hs
index 8f63915..df192c0 100644
--- a/source/Megalodon.hs
+++ b/source/Megalodon.hs
@@ -2,21 +2,19 @@ module Megalodon where
 
 import Base hiding (null)
 import Syntax.Internal
-import Syntax.Lexicon
 import Checking (makeReplacementIff)
 import Report.Location
 
 import Bound.Scope
 import Bound.Var
-import Data.Map.Strict qualified as Map
 import Data.List.NonEmpty qualified as NonEmpty
 import TextBuilder
 import Data.List qualified as List
 import Data.Text qualified as Text
 
 
-encodeBlocks :: Lexicon -> [Block] -> Text
-encodeBlocks lexi blocks = TextBuilder.toText (preamble <> buildBlocks lexi blocks)
+encodeBlocks :: [Block] -> Text
+encodeBlocks blocks = TextBuilder.toText (preamble <> buildBlocks blocks)
 
 closure :: [ExprOf VarSymbol] -> ExprOf VarSymbol -> Formula
 closure asms stmt = contraction (forallClosure mempty (makeConjunction asms `Implies` stmt))
@@ -25,44 +23,44 @@ unAsm :: Asm -> Formula
 unAsm (Asm phi) = phi
 unAsm (AsmStruct x sp) = TermSymbol Nowhere (SymbolPredicate (PredicateNounStruct sp)) [TermVar x]
 
-buildBlocks :: Lexicon -> [Block] -> TextBuilder
-buildBlocks lexi = \case
+buildBlocks :: [Block] -> TextBuilder
+buildBlocks = \case
     BlockAxiom _pos lbl (Axiom asms stmt) : blocks ->
         let phi = closure (unAsm <$> asms) stmt
-        in text "Fact " <> buildMarker lbl <> text " : " <> buildFormula lexi phi <> text ".\nAdmitted.\n" <> buildBlocks lexi blocks
+        in text "Fact " <> buildMarker lbl <> text " : " <> buildFormula phi <> text ".\nAdmitted.\n" <> buildBlocks blocks
     BlockLemma _pos lbl (Lemma asms stmt) : BlockProof _ _ _ : blocks ->
         let phi = closure (unAsm <$> asms) stmt
-        in text "Theorem " <> buildMarker lbl <> text " : " <> buildFormula lexi phi <> text ".\nAdmitted.\n" <> buildBlocks lexi blocks
+        in text "Theorem " <> buildMarker lbl <> text " : " <> buildFormula phi <> text ".\nAdmitted.\n" <> buildBlocks blocks
     BlockLemma _pos lbl (Lemma asms stmt) : blocks ->
         let phi = closure (unAsm <$> asms) stmt
-        in text "Theorem " <> buildMarker lbl <> text " : " <> buildFormula lexi phi <> text ".\nAdmitted.\n" <> buildBlocks lexi blocks
+        in text "Theorem " <> buildMarker lbl <> text " : " <> buildFormula phi <> text ".\nAdmitted.\n" <> buildBlocks blocks
     BlockDefn _pos _lbl defn : blocks->
-        buildDefn lexi defn <> buildBlocks lexi blocks
+        buildDefn defn <> buildBlocks blocks
     BlockAbbr _pos _lbl abbr : blocks->
-        buildAbbr lexi abbr <> buildBlocks lexi blocks
+        buildAbbr abbr <> buildBlocks blocks
     [] ->
         mempty
     block : _ ->
         _TODO ("builBlocks" <> show block)
 
-buildDefn :: Lexicon -> Defn -> TextBuilder
-buildDefn lexi = \case
+buildDefn :: Defn -> TextBuilder
+buildDefn = \case
     DefnPredicate [] predi xs phi ->
-        "Definition " <> buildSymbol lexi (SymbolPredicate predi) <> " := " <>
-        "fun " <> buildVarSymbols xs <> ": set => " <> buildFormula lexi phi <> ".\n"
+        "Definition " <> buildSymbol (SymbolPredicate predi) <> " := " <>
+        "fun " <> buildVarSymbols xs <> ": set => " <> buildFormula phi <> ".\n"
     DefnFun [] f xs phi ->
-        "Definition " <> buildSymbol lexi (SymbolFun f) <> " := " <>
-        buildSetFunIfNonEmpty (buildVarSymbols xs) (buildFormula lexi phi) <> ".\n"
+        "Definition " <> buildSymbol (SymbolFun f) <> " := " <>
+        buildSetFunIfNonEmpty (buildVarSymbols xs) (buildFormula phi) <> ".\n"
     DefnOp f xs phi ->
-        "Definition " <> buildSymbol lexi (SymbolMixfix f) <> " := " <>
-        buildSetFunIfNonEmpty (buildVarSymbols xs) (buildFormula lexi phi) <> ".\n"
+        "Definition " <> buildSymbol (SymbolMixfix f) <> " := " <>
+        buildSetFunIfNonEmpty (buildVarSymbols xs) (buildFormula phi) <> ".\n"
     _ ->
         error "assumptions in definition, deprecated"
 
-buildAbbr :: Lexicon -> Abbreviation -> TextBuilder
-buildAbbr lexi (Abbreviation f body) =
-    "Definition " <> buildSymbol lexi f <> " := " <>
-    buildSetFunIfNonEmpty buildBindings' (buildFormula lexi ((instantiate (TermVar . FreshVar) (fmap absurd body)))) <> ".\n"
+buildAbbr :: Abbreviation -> TextBuilder
+buildAbbr (Abbreviation f body) =
+    "Definition " <> buildSymbol f <> " := " <>
+    buildSetFunIfNonEmpty buildBindings' (buildFormula ((instantiate (TermVar . FreshVar) (fmap absurd body)))) <> ".\n"
         where
             buildBindings' :: TextBuilder
             buildBindings' = intercalate (char ' ') (buildVarSymbol . FreshVar <$> List.sort (List.nub (bindings body)))
@@ -70,62 +68,62 @@ buildAbbr lexi (Abbreviation f body) =
 buildSetFunIfNonEmpty :: TextBuilder -> TextBuilder -> TextBuilder
 buildSetFunIfNonEmpty xs b = if isEmpty xs then b else "fun " <> xs <> " : set => " <> b
 
-buildFormula :: Lexicon -> Formula -> TextBuilder
-buildFormula lexi = \case
+buildFormula :: Formula -> TextBuilder
+buildFormula = \case
     TermVar x -> buildVarSymbol x
     -- We handle eq in a special manner to avoid having to specify the type of the equality.
     TermSymbol _pos f [x,y] | isEqSymbol f ->
-        char '(' <> buildFormula lexi x <> text " = " <> buildFormula lexi y <> char ')'
+        char '(' <> buildFormula x <> text " = " <> buildFormula y <> char ')'
     TermSymbol _pos f [x,y] | isDiseqSymbol f ->
-        char '(' <> buildFormula lexi x <> text " <> " <> buildFormula lexi y <> char ')'
+        char '(' <> buildFormula x <> text " <> " <> buildFormula y <> char ')'
     TermSymbol _pos f es ->
-        let es' = buildSymbol lexi f : (buildFormula lexi <$> es)
+        let es' = buildSymbol f : (buildFormula <$> es)
         in char '(' <> intercalate (char ' ') es' <> char ')'
     Apply e es ->
-        let es' = NonEmpty.cons (buildFormula lexi e) (buildFormula lexi <$> es)
+        let es' = NonEmpty.cons (buildFormula e) (buildFormula <$> es)
         in char '(' <> intercalate (char ' ') es' <> char ')'
-    Not _pos e -> text "~(" <> buildFormula lexi e <> char ')'
+    Not _pos e -> text "~(" <> buildFormula e <> char ')'
     Connected conn e1 e2 ->
-        char '(' <> buildConn conn (buildFormula lexi e1) (buildFormula lexi e2) <> char ')'
+        char '(' <> buildConn conn (buildFormula e1) (buildFormula e2) <> char ')'
     Quantified quant body ->
-        char  '(' <> buildQuant quant <> char ' ' <> buildBindings body <> text ",(" <> buildFormula lexi (instantiate TermVar body) <> text "))"
+        char  '(' <> buildQuant quant <> char ' ' <> buildBindings body <> text ",(" <> buildFormula (instantiate TermVar body) <> text "))"
     TermSep x bound phi ->
-        char '{' <> buildVarSymbol x <> " :e (" <> buildFormula lexi bound <> text ")|" <> buildFormula lexi (instantiate1 (TermVar x) phi) <> char '}'
+        char '{' <> buildVarSymbol x <> " :e (" <> buildFormula bound <> text ")|" <> buildFormula (instantiate1 (TermVar x) phi) <> char '}'
     ReplacePred y x xB body ->
         let x' = buildVarSymbol x
             y' = buildVarSymbol y
             fromReplacementVar = \case
                 ReplacementDomVar -> TermVar x
                 ReplacementRangeVar -> TermVar y
-            body' = buildFormula lexi (instantiate fromReplacementVar body)
-        in "let MkReplFun := fun " <> x' <> " : set => (Eps_i (fun " <> y' <> "=>" <> body' <> ")) in {MkReplFun " <> x' <> "|" <> x' <> " :e (" <> buildFormula lexi xB <> ")}"
+            body' = buildFormula (instantiate fromReplacementVar body)
+        in "let MkReplFun := fun " <> x' <> " : set => (Eps_i (fun " <> y' <> "=>" <> body' <> ")) in {MkReplFun " <> x' <> "|" <> x' <> " :e (" <> buildFormula xB <> ")}"
     ReplaceFun ((x, xB) :| []) lhs cond ->
         let x' = buildVarSymbol x
-            xB' = "(" <> buildFormula lexi xB <> ")" -- parens probably not needed
-            lhs' = "(fun " <> x' <> " => " <> buildFormula lexi (instantiate TermVar lhs) <> ")"
-            cond' = "(fun " <> x' <> " => " <> buildFormula lexi (instantiate TermVar cond) <> ")"
+            xB' = "(" <> buildFormula xB <> ")" -- parens probably not needed
+            lhs' = "(fun " <> x' <> " => " <> buildFormula (instantiate TermVar lhs) <> ")"
+            cond' = "(fun " <> x' <> " => " <> buildFormula (instantiate TermVar cond) <> ")"
         -- Using "ReplSep : set->(set->prop)->(set->set)->set"
         in "ReplSep " <> xB' <> cond' <> lhs'
     ReplaceFun ((x, xB) :| (y, yB) : []) lhs cond ->
         let x' = buildVarSymbol x
-            xB' = "(" <> buildFormula lexi xB <> ")"
+            xB' = "(" <> buildFormula xB <> ")"
             y' = buildVarSymbol y
-            yB' = "(fun dummyVar => " <> buildFormula lexi yB <> ")"
-            lhs' = "(fun " <> x' <> " " <> y' <> " => " <> buildFormula lexi (instantiate TermVar lhs) <> ")"
-            cond' = "(fun " <> x' <> " " <> y' <> " => " <> buildFormula lexi (instantiate TermVar cond) <> ")"
+            yB' = "(fun dummyVar => " <> buildFormula yB <> ")"
+            lhs' = "(fun " <> x' <> " " <> y' <> " => " <> buildFormula (instantiate TermVar lhs) <> ")"
+            cond' = "(fun " <> x' <> " " <> y' <> " => " <> buildFormula (instantiate TermVar cond) <> ")"
         -- Using "ReplSep2 : set -> (set -> set) -> (set -> set -> prop) -> (set -> set -> set) -> set"
         in "ReplSep2 " <> xB' <> yB' <> cond' <> lhs'
     ReplaceFun bounds lhs cond ->
         -- Silly placeholder translation for now
         let iff = makeReplacementIff (TermVar (F "frs")) bounds lhs cond
-        in "Eps_i (fun frs : set => " <> buildFormula lexi iff <> ")"
+        in "Eps_i (fun frs : set => " <> buildFormula iff <> ")"
     Lambda _ -> text "TODO_buildFormula_Lambda"
     PropositionalConstant IsTop -> "True"
     PropositionalConstant IsBottom -> "False"
     TermSymbolStruct f me ->
         let f' = buildMarker (Marker (unStructSymbol f))
             e = me ?? error "unannotated struct op"
-        in char '(' <> f' <> buildFormula lexi e <> char ')'
+        in char '(' <> f' <> buildFormula e <> char ')'
 
 buildMarker :: Marker -> TextBuilder
 buildMarker (Marker m)= text m
@@ -138,10 +136,10 @@ buildQuant = \case
 buildBindings :: Scope VarSymbol ExprOf a -> TextBuilder
 buildBindings body = intercalate (char ' ') (buildVarSymbol <$> List.nub (bindings body))
 
-buildBounds :: Lexicon -> NonEmpty (VarSymbol, ExprOf VarSymbol) -> TextBuilder
-buildBounds l (bound :| bounds) = foldr (\b bs -> buildBound b <> "/\\ " <> bs) (buildBound bound) bounds
+buildBounds :: NonEmpty (VarSymbol, ExprOf VarSymbol) -> TextBuilder
+buildBounds (bound :| bounds) = foldr (\b bs -> buildBound b <> "/\\ " <> bs) (buildBound bound) bounds
     where
-        buildBound (y, yB) = buildVarSymbol y <> " :e (" <> buildFormula l yB <> ")"
+        buildBound (y, yB) = buildVarSymbol y <> " :e (" <> buildFormula yB <> ")"
 
 buildConn :: Connective -> (TextBuilder -> TextBuilder -> TextBuilder)
 buildConn conn = \p q -> case conn of
@@ -160,9 +158,9 @@ buildVarSymbol = \case
 buildVarSymbols :: (Functor t, Foldable t) => t VarSymbol -> TextBuilder
 buildVarSymbols xs = intercalate (char ' ') (fmap buildVarSymbol xs)
 
-buildSymbol :: Lexicon -> Symbol -> TextBuilder
-buildSymbol _ (SymbolInteger i) = decimal i
-buildSymbol lexi symb = fromRightMarker case symb of
+buildSymbol :: Symbol -> TextBuilder
+buildSymbol (SymbolInteger i) = decimal i
+buildSymbol symb = fromRightMarker case symb of
     SymbolMixfix f ->
         Right (mixfixMarker f)
     SymbolFun f -> Right (lexicalItemSgPlMarker f)
diff --git a/source/Provers.hs b/source/Provers.hs
index d675627..2c1e48c 100644
--- a/source/Provers.hs
+++ b/source/Provers.hs
@@ -136,7 +136,7 @@ timeDifferenceToText startTime endTime = nominalDiffTimeToText (diffUTCTime endT
 runProver :: (MonadIO io, MonadLogger io) => ProverInstance -> Task -> io (Formula, ProverAnswer)
 runProver prover@Prover{..} task = do
     startTime <- liftIO getCurrentTime
-    (exitCode, answer, answerErr) <- liftIO (runProverProcess proverPath proverArgs task)
+    (_exitCode, answer, answerErr) <- liftIO (runProverProcess proverPath proverArgs task)
     endTime <- liftIO getCurrentTime
     let duration = timeDifferenceToText startTime endTime