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

Documentation.SBV.Examples.KnuckleDragger.Kleene

Description

Example use of the KnuckleDragger 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

Data Kleene Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Kleene Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Kleene -> c Kleene # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Kleene # toConstr :: Kleene -> Constr # dataTypeOf :: Kleene -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Kleene) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kleene) # gmapT :: (forall b. Data b => b -> b) -> Kleene -> Kleene # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kleene -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kleene -> r # gmapQ :: (forall d. Data d => d -> u) -> Kleene -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Kleene -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Kleene -> m Kleene # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Kleene -> m Kleene # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Kleene -> m 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.KnuckleDragger.Kleene Methods (+) :: SKleene -> SKleene -> SKleene # (-) :: SKleene -> SKleene -> SKleene # (*) :: SKleene -> SKleene -> SKleene # negate :: SKleene -> SKleene # abs :: SKleene -> SKleene # signum :: SKleene -> SKleene # fromInteger :: Integer -> SKleene #
Read Kleene Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Kleene Methods readsPrec :: Int -> ReadS Kleene # readList :: ReadS [Kleene] # readPrec :: ReadPrec Kleene # readListPrec :: ReadPrec [Kleene] #
Show Kleene Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Kleene Methods showsPrec :: Int -> Kleene -> ShowS # show :: Kleene -> String # showList :: [Kleene] -> ShowS #
SymVal Kleene Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Kleene Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Kleene) Source # literal :: Kleene -> SBV Kleene Source # fromCV :: CV -> Kleene Source # isConcretely :: SBV Kleene -> (Kleene -> Bool) -> Bool 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 # isConcrete :: SBV Kleene -> Bool Source # isSymbolic :: SBV Kleene -> Bool Source #
HasKind Kleene Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.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 # isUserSort :: Kleene -> Bool Source # isChar :: Kleene -> Bool Source # isString :: Kleene -> Bool Source # isList :: Kleene -> Bool Source # isSet :: Kleene -> Bool Source # isTuple :: Kleene -> Bool Source # isMaybe :: Kleene -> Bool Source # isEither :: Kleene -> Bool Source # isArray :: Kleene -> Bool Source # showType :: Kleene -> String Source #
SatModel Kleene Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Kleene Methods parseCVs :: [CV] -> Maybe (Kleene, [CV]) Source # cvtModel :: (Kleene -> Maybe b) -> Maybe (Kleene, [CV]) -> Maybe (b, [CV]) Source #

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                             Q.E.D.
  Step  : 2                             Q.E.D.
  Step  : 3                             Q.E.D.
  Step  : 4                             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.