Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use Writer monad instead of State to annotate comments #47

Merged
merged 1 commit into from
Nov 9, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 9 additions & 9 deletions Codec/TPTP/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,11 @@
import Control.Applicative
import Control.Monad
import Control.Monad.Identity
import Control.Monad.State
import Control.Monad.Writer (Writer, runWriter)
import Data.Data
import Data.Function
import Data.Monoid hiding(All)
import Data.Semigroup (Semigroup)

Check warning on line 18 in Codec/TPTP/Base.hs

View workflow job for this annotation

GitHub Actions / build (8.10.7)

The import of ‘Data.Semigroup’ is redundant

Check warning on line 18 in Codec/TPTP/Base.hs

View workflow job for this annotation

GitHub Actions / build (9.2.8)

The import of ‘Data.Semigroup’ is redundant

Check warning on line 18 in Codec/TPTP/Base.hs

View workflow job for this annotation

GitHub Actions / build (9.8.2)

The import of ‘Data.Semigroup’ is redundant

Check warning on line 18 in Codec/TPTP/Base.hs

View workflow job for this annotation

GitHub Actions / build (9.0.2)

The import of ‘Data.Semigroup’ is redundant

Check warning on line 18 in Codec/TPTP/Base.hs

View workflow job for this annotation

GitHub Actions / build (8.8.4)

The import of ‘Data.Semigroup’ is redundant

Check warning on line 18 in Codec/TPTP/Base.hs

View workflow job for this annotation

GitHub Actions / build (9.6.6)

The import of ‘Data.Semigroup’ is redundant

Check warning on line 18 in Codec/TPTP/Base.hs

View workflow job for this annotation

GitHub Actions / build (9.4.8)

The import of ‘Data.Semigroup’ is redundant
import Data.Set as S hiding(fold)
import Data.String
import Prelude --hiding(concat,foldl,foldl1,foldr,foldr1)
Expand All @@ -34,21 +34,21 @@
-- * Formulae and terms decorated with state

-- | First-order formulae decorated with state
type FormulaST s = F (State s)
type FormulaW s = F (Writer s)

-- | Terms decorated with state
type TermST s = T (State s)
type TermW s = T (Writer s)

-- | First-order formulae decorated with comments
type FormulaC = FormulaST [String]
type FormulaC = FormulaW [String]

-- | Terms decorated with comments
type TermC = TermST [String]
type TermC = TermW [String]

-- | Forget comments in formulae decorated with comments
forgetFC :: FormulaC -> Formula
forgetFC (F f) = F . return $
case evalState f [] of
case fst $ runWriter f of
BinOp f1 op f2 -> BinOp (forgetFC f1) op (forgetFC f2)
InfixPred t1 pred_ t2 -> InfixPred (forgetTC t1) pred_ (forgetTC t2)
PredApp aw ts -> PredApp aw (fmap forgetTC ts)
Expand All @@ -58,7 +58,7 @@
-- | Forget comments in terms decorated with comments
forgetTC :: TermC -> Term
forgetTC (T t) = T . return $
case evalState t [] of
case fst $ runWriter t of
Var v -> Var v
NumberLitTerm d -> NumberLitTerm d
DistinctObjectTerm s -> DistinctObjectTerm s
Expand Down Expand Up @@ -216,8 +216,8 @@
deriving (Eq,Ord,Show,Read,Data,Typeable)
-}

-- | A line of a TPTP file: Annotated formula (with the comment string embbeded in the State monad ), comment or include statement
type TPTP_Input_C = TPTP_Input_ (State [String])
-- | A line of a TPTP file: Annotated formula (with the comment string embbeded in the Writer monad ), comment or include statement
type TPTP_Input_C = TPTP_Input_ (Writer [String])

-- | Forget comments in a line of a TPTP file decorated with comments
forgetTIC :: TPTP_Input_C -> TPTP_Input
Expand Down
6 changes: 3 additions & 3 deletions ParserC.y
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ import Codec.TPTP.Base
import System.IO
import System.IO.Unsafe
import Control.Monad.Identity
import Control.Monad.State
import Control.Monad.Writer
}

%name parseTPTPwithComment
Expand Down Expand Up @@ -505,8 +505,8 @@ class Commented c where
instance Commented Identity where
withComments = const

instance Commented (State [String]) where
withComments (F mf) s = F $ do { f <- mf; put s; return f }
instance Commented (Writer [String]) where
withComments (F mf) s = F $ do { f <- mf; tell s; return f }
Comment on lines -508 to +509
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The behavior appears to change from “replace” to “append,” but in reality, there is no difference.

The only place withComments is used is

logic-TPTP/ParserC.y

Lines 148 to 150 in b02af74

quantified_formula :: {FormulaC}
quantified_formula : quantifier lbra variable_list rbra colon unitary_formula
{ $1 $3 $6 `withComments` comm $5 }

and the quantifier is defined as

logic-TPTP/ParserC.y

Lines 188 to 189 in b02af74

quantifier :: {[V] -> FormulaC -> FormulaC}
quantifier : exclam { for_all } | question { exists }

and for_all / exists are defined as:

-- | Universal quantification
for_all :: Pointed c => [V] -> (F c) -> F c
for_all vars x = (F . point) $ Quant All vars x
-- | Existential quantification
exists :: Pointed c => [V] -> (F c) -> F c
exists vars x = (F . point) $ Quant Exists vars x

Therefore, mf in the above code is always point of something, i.e. the annotation is empty.



stripQuotes which (x:xs) = go xs
Expand Down
1 change: 1 addition & 0 deletions changelog.markdown
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
## 0.6.0.0

* migrate to `prettyprinter` package family from `ansi-wl-pprint` package
* Use `Writer` moand instead of `State` to annotate comments

## 0.5.1.0

Expand Down
Loading