Portability | GHC only |
---|---|
Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
Safe Haskell | None |
Guarded formulas.
- data Guarded s c v
- type LGuarded c = Guarded (String, LSort) c LVar
- type LNGuarded = Guarded (String, LSort) Name LVar
- data GAtom t
- gfalse :: Guarded s c v
- gtrue :: Guarded s c v
- gdisj :: (Ord s, Ord c, Ord v) => [Guarded s c v] -> Guarded s c v
- gconj :: (Ord s, Ord c, Ord v) => [Guarded s c v] -> Guarded s c v
- gex :: (Ord s, Ord c, Ord v) => [s] -> [Atom (VTerm c (BVar v))] -> Guarded s c v -> Guarded s c v
- gall :: (Eq s, Eq c, Eq v) => [s] -> [Atom (VTerm c (BVar v))] -> Guarded s c v -> Guarded s c v
- gnot :: (Ord s, Ord c, Ord v) => Guarded s c v -> Guarded s c v
- ginduct :: Ord c => LGuarded c -> Either String (LGuarded c, LGuarded c)
- formulaToGuarded :: HighlightDocument d => LNFormula -> Either d LNGuarded
- formulaToGuarded_ :: LNFormula -> LNGuarded
- simplifyGuarded :: (LNAtom -> Maybe Bool) -> LNGuarded -> Maybe LNGuarded
- mapGuardedAtoms :: (Integer -> Atom (VTerm c (BVar v)) -> Atom (VTerm d (BVar w))) -> Guarded s c v -> Guarded s d w
- atomToGAtom :: Show t => Atom t -> GAtom t
- sortGAtoms :: [GAtom t] -> [GAtom t]
- isConjunction :: Guarded s c v -> Bool
- isDisjunction :: Guarded s c v -> Bool
- isAllGuarded :: Guarded s c v -> Bool
- isExGuarded :: Guarded s c v -> Bool
- isSafetyFormula :: HasFrees (Guarded s c v) => Guarded s c v -> Bool
- guardFactTags :: Guarded s c v -> [FactTag]
- bvarToLVar :: Ord c => Atom (VTerm c (BVar LVar)) -> Atom (VTerm c LVar)
- openGuarded :: (Ord c, MonadFresh m) => LGuarded c -> m (Maybe (Quantifier, [LVar], [Atom (VTerm c LVar)], LGuarded c))
- substBound :: Ord c => [(Integer, LVar)] -> LGuarded c -> LGuarded c
- substBoundAtom :: Ord c => [(Integer, LVar)] -> Atom (VTerm c (BVar LVar)) -> Atom (VTerm c (BVar LVar))
- substFree :: Ord c => [(LVar, Integer)] -> LGuarded c -> LGuarded c
- substFreeAtom :: Ord c => [(LVar, Integer)] -> Atom (VTerm c (BVar LVar)) -> Atom (VTerm c (BVar LVar))
- prettyGuarded :: HighlightDocument d => LNGuarded -> d
Guarded formulas
GAto (Atom (VTerm c (BVar v))) | |
GDisj (Disj (Guarded s c v)) | |
GConj (Conj (Guarded s c v)) | |
GGuarded Quantifier [s] [Atom (VTerm c (BVar v))] (Guarded s c v) | Denotes |
Apply LNGuarded | |
Foldable (Guarded s c) | |
(Eq s, Eq c, Eq v) => Eq (Guarded s c v) | |
(Ord s, Ord c, Ord v) => Ord (Guarded s c v) | |
(Show s, Show c, Show v) => Show (Guarded s c v) | |
(Binary s_1627723903, Binary c_1627723904, Binary v_1627723905) => Binary (Guarded s_1627723903 c_1627723904 v_1627723905) | |
(NFData s_1627723903, NFData c_1627723904, NFData v_1627723905) => NFData (Guarded s_1627723903 c_1627723904 v_1627723905) | |
Ord c => HasFrees (Guarded (String, LSort) c LVar) |
Atoms that are allowed as guards.
Smart constructors
gdisj :: (Ord s, Ord c, Ord v) => [Guarded s c v] -> Guarded s c vSource
gdisj gfs
smart constructor for the disjunction of gfs.
gconj :: (Ord s, Ord c, Ord v) => [Guarded s c v] -> Guarded s c vSource
gconj gfs
smart constructor for the conjunction of gfs.
gex :: (Ord s, Ord c, Ord v) => [s] -> [Atom (VTerm c (BVar v))] -> Guarded s c v -> Guarded s c vSource
gall :: (Eq s, Eq c, Eq v) => [s] -> [Atom (VTerm c (BVar v))] -> Guarded s c v -> Guarded s c vSource
ginduct :: Ord c => LGuarded c -> Either String (LGuarded c, LGuarded c)Source
Try to prove the formula by applying induction over the trace.
Returns
if this is not possible. Returns a tuple of
formulas: one formalizing the proof obligation of the base-case and one
formalizing the proof obligation of the step-case.
Left
errMsg
formulaToGuarded :: HighlightDocument d => LNFormula -> Either d LNGuardedSource
formulaToGuarded fm
returns a guarded formula gf
that is
equivalent to fm
if possible.
formulaToGuarded_ :: LNFormula -> LNGuardedSource
formulaToGuarded fm
returns a guarded formula gf
that is
equivalent to fm
under the assumption that this is possible.
If not, then error
is called.
Transformation
:: (LNAtom -> Maybe Bool) | Partial assignment for truth value of atoms. |
-> LNGuarded | Original formula |
-> Maybe LNGuarded | Simplified formula, provided some simplification was performed. |
Simplify a Guarded
formula by replacing atoms with their truth value,
if it can be determined.
mapGuardedAtoms :: (Integer -> Atom (VTerm c (BVar v)) -> Atom (VTerm d (BVar w))) -> Guarded s c v -> Guarded s d wSource
Map a guarded formula with scope info. The Integer argument denotes the number of quantifiers that have been encountered so far.
sortGAtoms :: [GAtom t] -> [GAtom t]Source
Stable sort that ensures that actions occur before equations.
Queries
isConjunction :: Guarded s c v -> BoolSource
isDisjunction :: Guarded s c v -> BoolSource
isAllGuarded :: Guarded s c v -> BoolSource
isExGuarded :: Guarded s c v -> BoolSource
isSafetyFormula :: HasFrees (Guarded s c v) => Guarded s c v -> BoolSource
Check whether the guarded formula is closed and does not contain an
existential quantifier. This under-approximates the question whether the
formula is a safety formula. A safety formula phi
has the property that a
trace violating it can never be extended to a trace satisfying it.
guardFactTags :: Guarded s c v -> [FactTag]Source
All FactTag
s that are used in guards.
Conversions to non-bound representations
bvarToLVar :: Ord c => Atom (VTerm c (BVar LVar)) -> Atom (VTerm c LVar)Source
Assuming that there are no more bound variables left in an atom of a formula, convert it to an atom with free variables only.
openGuarded :: (Ord c, MonadFresh m) => LGuarded c -> m (Maybe (Quantifier, [LVar], [Atom (VTerm c LVar)], LGuarded c))Source
openGuarded gf
returns Just (qua,vs,ats,gf')
if gf
is a guarded
clause and Nothing
otherwise. In the first case, qua
is the quantifier,
vs
is a list of fresh variables, ats
is the antecedent, and gf'
is the
succedent. In both antecedent and succedent, the bound variables are
replaced by vs
.
Substitutions
substBound :: Ord c => [(Integer, LVar)] -> LGuarded c -> LGuarded cSource
substBound s gf
substitutes each occurence of a bound
variable i
in dom(s)
with the corresponding free variable
s(i)=x
in all atoms in gf
.
substBoundAtom :: Ord c => [(Integer, LVar)] -> Atom (VTerm c (BVar LVar)) -> Atom (VTerm c (BVar LVar))Source
substBoundAtom s a
substitutes each occurence of a bound variables i
in dom(s)
with the corresponding free variable x=s(i)
in the atom a
.
substFree :: Ord c => [(LVar, Integer)] -> LGuarded c -> LGuarded cSource
substFreeAtom s gf
substitutes each occurence of a free variables
v in dom(s)
with the correpsonding bound variables i=s(v)
in all atoms in gf
.
substFreeAtom :: Ord c => [(LVar, Integer)] -> Atom (VTerm c (BVar LVar)) -> Atom (VTerm c (BVar LVar))Source
substFreeAtom s a
substitutes each occurence of a free variables v
in dom(s)
with the bound variables i=s(v)
in the atom a
.
Pretty-printing
:: HighlightDocument d | |
=> LNGuarded | Guarded Formula. |
-> d | Pretty printed formula. |
Pretty print a formula.