This library parses string to formulas
Formula can be
Signed with T[rue] or F[alse]
Parse string to Formula
Parse string to Signed Formula
Show representation of a Formula. todo: rewrite with toString instead.
Show representation of a Signed Formula. todo: rewrite with toString instead.
Return error message from parsing error
Is the formula of type Alpha
Is the formula of type Beta
Are the two signed formulas complementary
Is the first signed formula of the other
Get formula out of signed formula
Get signed subformulas as list of signed formulas
module Formula
exposing
( Formula(..)
, Signed(..)
, isAlpha
, isBeta
, signedSubformulas
, isSignedSubformulaOf
, isSignedComplementary
, signedGetFormula
, parseSigned
, parse
, errorString
, strSigned
, strFormula
)
{-| This library parses string to formulas
# Definitions
@docs Formula, Signed
# Parsers
@docs parse, parseSigned
# Strings
@docs strFormula, strSigned, errorString
# Helpers
@docs isAlpha, isBeta, isSignedComplementary, isSignedSubformulaOf, signedGetFormula, signedSubformulas
-}
{- todo: in the future, we may expose
, SignedType(..)
, subformulas
, isSubformulaOf
, negType
, negSigned
, signedType
-}
import Char
import Set
import Parser
exposing
( Parser
, (|.)
, (|=)
, succeed
, symbol
, float
, ignore
, zeroOrMore
, oneOf
, lazy
, keyword
, delayedCommitMap
, end
, oneOrMore
)
import Parser.LanguageKit exposing (variable, sequence, whitespace)
{-| Formula can be
- atomic
- negation of a formula
- disjunction, conjuction, implication of two formulas
- FF and FT
-}
type Formula
= Atom String
| Neg Formula
| Disj Formula Formula
| Conj Formula Formula
| Impl Formula Formula
| FF
| FT
subformulas : Formula -> List Formula
subformulas f =
case f of
Neg sf ->
[ sf ]
Disj lf rf ->
[ lf, rf ]
Conj lf rf ->
[ lf, rf ]
Impl lf rf ->
[ lf, rf ]
_ ->
[]
isSubformulaOf : Formula -> Formula -> Bool
isSubformulaOf a b =
List.member a (subformulas b)
--
-- Signed formulas
--
{-| Signed with T[rue] or F[alse]
-}
type Signed a
= T a
| F a
type SignedType
= Alpha
| Beta
negType : SignedType -> SignedType
negType t =
case t of
Alpha ->
Beta
Beta ->
Alpha
negSigned : Signed Formula -> Signed Formula
negSigned sf =
case sf of
T f ->
F f
F f ->
T f
signedType : Signed Formula -> SignedType
signedType sf =
case sf of
T FF ->
Alpha
T FT ->
Alpha
T (Atom _) ->
Alpha
F (Atom _) ->
Alpha
T (Neg _) ->
Alpha
F (Neg _) ->
Alpha
T (Conj _ _) ->
Alpha
T (Disj _ _) ->
Beta
T (Impl _ _) ->
Beta
F f ->
negType <| signedType <| T f
{-| Is the formula of type Alpha
-}
isAlpha : Signed Formula -> Bool
isAlpha x =
Alpha == signedType x
{-| Is the formula of type Beta
-}
isBeta : Signed Formula -> Bool
isBeta x =
Beta == signedType x
{-| Get signed subformulas as list of signed formulas
-}
signedSubformulas : Signed Formula -> List (Signed Formula)
signedSubformulas sf =
case sf of
T (Neg f) ->
[ F f ]
T (Conj l r) ->
[ T l, T r ]
T (Disj l r) ->
[ T l, T r ]
T (Impl l r) ->
[ F l, T r ]
T _ ->
[]
F f ->
T f |> signedSubformulas |> List.map negSigned
{-| Is the first signed formula of the other
-}
isSignedSubformulaOf : Signed Formula -> Signed Formula -> Bool
isSignedSubformulaOf a b =
List.member a (signedSubformulas b)
{-| Are the two signed formulas complementary
-}
isSignedComplementary : Signed Formula -> Signed Formula -> Bool
isSignedComplementary a b =
case ( a, b ) of
( T x, F y ) ->
x == y
( F x, T y ) ->
x == y
_ ->
False
{-| Get formula out of signed formula
-}
signedGetFormula : Signed Formula -> Formula
signedGetFormula sf =
case sf of
T f ->
f
F f ->
f
--
-- Parsing
--
{-| Parse string to Signed Formula
-}
parseSigned : String -> Result Parser.Error (Signed Formula)
parseSigned =
Parser.run (succeed identity |. spaces |= signedFormula |. spaces |. end)
signedFormula =
succeed identity
|. spaces
|= oneOf
[ succeed T
|. keyword "T"
|. spaces
|= formula
, succeed F
|. keyword "F"
|. spaces
|= formula
]
{-| Parse string to Formula
-}
parse : String -> Result Parser.Error Formula
parse =
Parser.run (succeed identity |. spaces |= formula |. spaces |. end)
{-| Return error message from parsing error
-}
errorString : Parser.Error -> String
errorString e =
"Invalid formula: " ++ (toString e)
formula : Parser Formula
formula =
oneOf
[ succeed Atom
|= variable Char.isLower Char.isLower (Set.fromList [])
, succeed Neg
|. oneOfSymbols [ "-", "¬", "~" ]
|. spaces
|= lazy (\_ -> formula)
, lazy (\_ -> binary [ "&", "∧", "/\\" ] Conj)
, lazy (\_ -> binary [ "|", "∨", "\\/" ] Disj)
, lazy (\_ -> binary [ "->", "→" ] Impl)
, succeed identity
|. symbol "("
|. spaces
|= lazy (\_ -> formula)
|. spaces
|. symbol ")"
]
binary conn constructor =
delayedCommitMap constructor
(succeed identity
|. symbol "("
|. spaces
|= lazy (\_ -> formula)
|. spaces
)
<|
succeed identity
|. oneOfSymbols conn
|. spaces
|= lazy (\_ -> formula)
|. spaces
|. symbol ")"
oneOfSymbols syms =
oneOf (List.map symbol syms)
spaces : Parser ()
spaces =
ignore zeroOrMore (\char -> char == ' ')
{-| Show representation of a Signed Formula. todo: rewrite with toString instead.
-}
strSigned : Signed Formula -> String
strSigned sf =
case sf of
T f ->
"T " ++ (strFormula f)
F f ->
"F " ++ (strFormula f)
{-| Show representation of a Formula. todo: rewrite with toString instead.
-}
strFormula : Formula -> String
strFormula f =
case f of
FT ->
"True"
FF ->
"False"
Atom a ->
a
Neg f ->
"¬" ++ (strFormula f)
Conj lf rf ->
"(" ++ (strFormula lf) ++ "∧" ++ (strFormula rf) ++ ")"
Disj lf rf ->
"(" ++ (strFormula lf) ++ "∨" ++ (strFormula rf) ++ ")"
Impl lf rf ->
"(" ++ (strFormula lf) ++ "→" ++ (strFormula rf) ++ ")"
--
-- helper funcs
--
sf : String -> Signed Formula
sf =
parseSigned >> Result.withDefault (T FF)
f : String -> Formula
f =
parse >> Result.withDefault FF
{- vim: set sw=2 ts=2 sts=2 et : -}