This is an alternative site for discovering Elm packages. You may be looking for the official Elm package site instead.
README

Formula

This library parses string to formulas

Definitions

type Formula = Atom String | Neg Formula | Disj Formula Formula | Conj Formula Formula | Impl Formula Formula | FF | FT

Formula can be

  • atomic
  • negation of a formula
  • disjunction, conjuction, implication of two formulas
  • FF and FT
type Signed a = T a | F a

Signed with T[rue] or F[alse]

Parsers

parse : String -> Result Parser.Error Formula

Parse string to Formula

parseSigned : String -> Result Parser.Error (Signed Formula)

Parse string to Signed Formula

Strings

strFormula : Formula -> String

Show representation of a Formula. todo: rewrite with toString instead.

strSigned : Signed Formula -> String

Show representation of a Signed Formula. todo: rewrite with toString instead.

errorString : Parser.Error -> String

Return error message from parsing error

Helpers

isAlpha : Signed Formula -> Bool

Is the formula of type Alpha

isBeta : Signed Formula -> Bool

Is the formula of type Beta

isSignedComplementary : Signed Formula -> Signed Formula -> Bool

Are the two signed formulas complementary

isSignedSubformulaOf : Signed Formula -> Signed Formula -> Bool

Is the first signed formula of the other

signedGetFormula : Signed Formula -> Formula

Get formula out of signed formula

signedSubformulas : Signed Formula -> List (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 : -}