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.