Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.TP.Kleene

Description

Example use of the TP layer, proving some Kleene algebra theorems.

Based on http://www.philipzucker.com/bryzzowski_kat/

Synopsis

Documentation

data Kleene Source #

An uninterpreted sort, corresponding to the type of Kleene algebra strings.

Instances

Instances details

Arbitrary Kleene Source #
Instance details Defined in Documentation.SBV.Examples.TP.Kleene Methods arbitrary :: Gen Kleene # shrink :: Kleene -> [Kleene] #
Num SKleene Source #	The `Num` instance for Kleene makes it easy to write regular expressions in the more familiar form.
Instance details Defined in Documentation.SBV.Examples.TP.Kleene Methods (+) :: SKleene -> SKleene -> SKleene # (-) :: SKleene -> SKleene -> SKleene # (*) :: SKleene -> SKleene -> SKleene # negate :: SKleene -> SKleene # abs :: SKleene -> SKleene # signum :: SKleene -> SKleene # fromInteger :: Integer -> SKleene #
SymVal Kleene Source #
Instance details Defined in Documentation.SBV.Examples.TP.Kleene Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Kleene) Source # mkSymValInit :: State -> SBV Kleene -> IO () Source # literal :: Kleene -> SBV Kleene Source # fromCV :: CV -> Kleene Source # isConcretely :: SBV Kleene -> (Kleene -> Bool) -> Bool Source # minMaxBound :: Maybe (Kleene, Kleene) Source # free :: MonadSymbolic m => String -> m (SBV Kleene) Source # free_ :: MonadSymbolic m => m (SBV Kleene) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Kleene] Source # symbolic :: MonadSymbolic m => String -> m (SBV Kleene) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Kleene] Source # unliteral :: SBV Kleene -> Maybe Kleene Source # unlitCV :: SBV Kleene -> Maybe (Kind, CVal) Source # isConcrete :: SBV Kleene -> Bool Source # isSymbolic :: SBV Kleene -> Bool Source #
HasKind Kleene Source #
Instance details Defined in Documentation.SBV.Examples.TP.Kleene Methods kindOf :: Kleene -> Kind Source # hasSign :: Kleene -> Bool Source # intSizeOf :: Kleene -> Int Source # isBoolean :: Kleene -> Bool Source # isBounded :: Kleene -> Bool Source # isReal :: Kleene -> Bool Source # isFloat :: Kleene -> Bool Source # isDouble :: Kleene -> Bool Source # isRational :: Kleene -> Bool Source # isFP :: Kleene -> Bool Source # isUnbounded :: Kleene -> Bool Source # isADT :: Kleene -> Bool Source # isChar :: Kleene -> Bool Source # isString :: Kleene -> Bool Source # isList :: Kleene -> Bool Source # isSet :: Kleene -> Bool Source # isTuple :: Kleene -> Bool Source # isArray :: Kleene -> Bool Source # isRoundingMode :: Kleene -> Bool Source # isUninterpreted :: Kleene -> Bool Source # showType :: Kleene -> String Source #

cv2Kleene :: String -> [CV] -> Kleene Source #

Conversion from SMT values to Kleene values.

_undefiner_Kleene :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SKleene = SBV Kleene Source #

Symbolic version of the type Kleene.

star :: SKleene -> SKleene Source #

Star operator over kleene algebras. We're leaving this uninterpreted.

(<=) :: SKleene -> SKleene -> SBool Source #

The set of strings matched by one regular expression is a subset of the second, if adding it to the second doesn't change the second set.

kleeneProofs :: IO () Source #

A sequence of Kleene algebra proofs. See http://www.cs.cornell.edu/~kozen/Papers/ka.pdf

We have:

>>> kleeneProofs
Axiom: par_assoc
Axiom: par_comm
Axiom: par_idem
Axiom: par_zero
Axiom: seq_assoc
Axiom: seq_zero
Axiom: seq_one
Axiom: rdistrib
Axiom: ldistrib
Axiom: unfold
Axiom: least_fix
Lemma: par_lzero                        Q.E.D.
Lemma: par_monotone                     Q.E.D.
Lemma: seq_monotone                     Q.E.D.
Lemma: star_star_1
  Step: 1 (unfold)                      Q.E.D.
  Step: 2 (factor out x * star x)       Q.E.D.
  Step: 3 (par_idem)                    Q.E.D.
  Step: 4 (unfold)                      Q.E.D.
  Result:                               Q.E.D.
Lemma: subset_eq                        Q.E.D.
Lemma: star_star_2_2                    Q.E.D.
Lemma: star_star_2_3                    Q.E.D.
Lemma: star_star_2_1                    Q.E.D.
Lemma: star_star_2                      Q.E.D.