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

Documentation.SBV.Examples.TP.VM

Contents

Language
Symbolic accessors
Environment and the stack
Interpretation
Virtual machine
Compilation
Correctness of the compiler

Description

Correctness of a simple interpreter vs virtual-machine interpretation of a language.

Synopsis

data Expr nm val
- = Var {
  - var :: nm
  }
- | Con {
  - con :: val
  }
- | Sqr {
  - sqrVal :: Expr nm val
  }
- | Inc {
  - incVal :: Expr nm val
  }
- | Add {
  - add1 :: Expr nm val
  - add2 :: Expr nm val
  }
- | Mul {
  - mul1 :: Expr nm val
  - mul2 :: Expr nm val
  }
- | Let {
  - lvar :: nm
  - lval :: Expr nm val
  - lbody :: Expr nm val
  }
type SExpr nm val = SBV (Expr nm val)
size :: (SymVal nm, SymVal val) => SExpr nm val -> SInteger
sCaseExpr :: (Mergeable result, SymVal nm, SymVal val) => SBV (Expr nm val) -> (SBV nm -> result) -> (SBV val -> result) -> (SBV (Expr nm val) -> result) -> (SBV (Expr nm val) -> result) -> (SBV (Expr nm val) -> SBV (Expr nm val) -> result) -> (SBV (Expr nm val) -> SBV (Expr nm val) -> result) -> (SBV nm -> SBV (Expr nm val) -> SBV (Expr nm val) -> result) -> result
isVar :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool
sVar :: (SymVal nm, SymVal val) => SBV nm -> SBV (Expr nm val)
getVar_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV nm
svar :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV nm
isCon :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool
sCon :: (SymVal nm, SymVal val) => SBV val -> SBV (Expr nm val)
getCon_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV val
scon :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV val
isSqr :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool
sSqr :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
getSqr_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
ssqrVal :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
isInc :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool
sInc :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
getInc_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
sincVal :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
isAdd :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool
sAdd :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val)
getAdd_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
getAdd_2 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
sadd1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
sadd2 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
isMul :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool
sMul :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val)
getMul_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
getMul_2 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
smul1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
smul2 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
isLet :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool
sLet :: (SymVal nm, SymVal val) => SBV nm -> SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val)
getLet_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV nm
getLet_2 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
getLet_3 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
slvar :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV nm
slval :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
slbody :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val)
type Env nm val = SList (nm, val)
type Stack val = SList val
interpInEnv :: (SymVal nm, SymVal val, Num (SBV val)) => Env nm val -> SExpr nm val -> SBV val
interp :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SBV val
data Instr nm val
- = IPushN {
  - ivar :: nm
  }
- | IPushV {
  - ival :: val
  }
- | IDup
- | IAdd
- | IMul
- | IBind nm
- | IForget
type SInstr nm val = SBV (Instr nm val)
compile :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SList (Instr nm val)
compileAndRun :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SBV val
correctness :: (SymVal nm, SymVal val, Num (SBV val)) => TP (Proof (Forall "expr" (Expr nm val) -> SBool))

Language

data Expr nm val Source #

Basic expression language.

Constructors

Var	Variables
Fields var :: nm
Con	Constants
Fields con :: val
Sqr	Squaring
Fields sqrVal :: Expr nm val
Inc	Increment
Fields incVal :: Expr nm val
Add	Addition
Fields add1 :: Expr nm val add2 :: Expr nm val
Mul	Addition
Fields mul1 :: Expr nm val mul2 :: Expr nm val
Let	Let expression
Fields lvar :: nm lval :: Expr nm val lbody :: Expr nm val

Instances

Instances details

Arbitrary (Expr nm val) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods arbitrary :: Gen (Expr nm val) # shrink :: Expr nm val -> [Expr nm val] #
(SymVal nm, SymVal val) => SymVal (Expr nm val) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV (Expr nm val)) Source # mkSymValInit :: State -> SBV (Expr nm val) -> IO () Source # literal :: Expr nm val -> SBV (Expr nm val) Source # fromCV :: CV -> Expr nm val Source # isConcretely :: SBV (Expr nm val) -> (Expr nm val -> Bool) -> Bool Source # minMaxBound :: Maybe (Expr nm val, Expr nm val) Source # free :: MonadSymbolic m => String -> m (SBV (Expr nm val)) Source # free_ :: MonadSymbolic m => m (SBV (Expr nm val)) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV (Expr nm val)] Source # symbolic :: MonadSymbolic m => String -> m (SBV (Expr nm val)) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV (Expr nm val)] Source # unliteral :: SBV (Expr nm val) -> Maybe (Expr nm val) Source # unlitCV :: SBV (Expr nm val) -> Maybe (Kind, CVal) Source # isConcrete :: SBV (Expr nm val) -> Bool Source # isSymbolic :: SBV (Expr nm val) -> Bool Source #
(HasKind nm, HasKind val) => HasKind (Expr nm val) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods kindOf :: Expr nm val -> Kind Source # hasSign :: Expr nm val -> Bool Source # intSizeOf :: Expr nm val -> Int Source # isBoolean :: Expr nm val -> Bool Source # isBounded :: Expr nm val -> Bool Source # isReal :: Expr nm val -> Bool Source # isFloat :: Expr nm val -> Bool Source # isDouble :: Expr nm val -> Bool Source # isRational :: Expr nm val -> Bool Source # isFP :: Expr nm val -> Bool Source # isUnbounded :: Expr nm val -> Bool Source # isADT :: Expr nm val -> Bool Source # isChar :: Expr nm val -> Bool Source # isString :: Expr nm val -> Bool Source # isList :: Expr nm val -> Bool Source # isSet :: Expr nm val -> Bool Source # isTuple :: Expr nm val -> Bool Source # isArray :: Expr nm val -> Bool Source # isRoundingMode :: Expr nm val -> Bool Source # isUninterpreted :: Expr nm val -> Bool Source # showType :: Expr nm val -> String Source #
(SymVal nm, SymVal val) => HasInductionSchema (Forall ta (Expr nm val) -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Expr nm val) -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT) => HasInductionSchema (Forall ta (Expr nm val) -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Expr nm val) -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

type SExpr nm val = SBV (Expr nm val) Source #

Symbolic version of the type Expr.

size :: (SymVal nm, SymVal val) => SExpr nm val -> SInteger Source #

Size of an expression. Used in strong induction.

Symbolic accessors

sCaseExpr :: (Mergeable result, SymVal nm, SymVal val) => SBV (Expr nm val) -> (SBV nm -> result) -> (SBV val -> result) -> (SBV (Expr nm val) -> result) -> (SBV (Expr nm val) -> result) -> (SBV (Expr nm val) -> SBV (Expr nm val) -> result) -> (SBV (Expr nm val) -> SBV (Expr nm val) -> result) -> (SBV nm -> SBV (Expr nm val) -> SBV (Expr nm val) -> result) -> result Source #

Case analyzer for the type Expr.

isVar :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool Source #

Field recognizer predicate.

sVar :: (SymVal nm, SymVal val) => SBV nm -> SBV (Expr nm val) Source #

Symbolic version of the constructor Var.

getVar_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV nm Source #

Field accessor function.

svar :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV nm Source #

Field accessor function.

isCon :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool Source #

Field recognizer predicate.

sCon :: (SymVal nm, SymVal val) => SBV val -> SBV (Expr nm val) Source #

Symbolic version of the constructor Con.

getCon_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV val Source #

Field accessor function.

scon :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV val Source #

Field accessor function.

isSqr :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool Source #

Field recognizer predicate.

sSqr :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Symbolic version of the constructor Sqr.

getSqr_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

ssqrVal :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

isInc :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool Source #

Field recognizer predicate.

sInc :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Symbolic version of the constructor Inc.

getInc_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

sincVal :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

isAdd :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool Source #

Field recognizer predicate.

sAdd :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val) Source #

Symbolic version of the constructor Add.

getAdd_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

getAdd_2 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

sadd1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

sadd2 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

isMul :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool Source #

Field recognizer predicate.

sMul :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val) Source #

Symbolic version of the constructor Mul.

getMul_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

getMul_2 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

smul1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

smul2 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

isLet :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool Source #

Field recognizer predicate.

sLet :: (SymVal nm, SymVal val) => SBV nm -> SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val) Source #

Symbolic version of the constructor Let.

getLet_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV nm Source #

Field accessor function.

getLet_2 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

getLet_3 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

slvar :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV nm Source #

Field accessor function.

slval :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

slbody :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

Environment and the stack

type Env nm val = SList (nm, val) Source #

Environment, binding names to values

type Stack val = SList val Source #

Stack of values.

Interpretation

interpInEnv :: (SymVal nm, SymVal val, Num (SBV val)) => Env nm val -> SExpr nm val -> SBV val Source #

Interpreter, in the usual functional style, taking an arbitrary environment.

interp :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SBV val Source #

Interpret starting from empty environment.

Virtual machine

data Instr nm val Source #

Instructions

Constructors

IPushN	Push the value of nm from the environment on to the stack
Fields ivar :: nm
IPushV	Push a value on to the stack
Fields ival :: val
IDup	Duplicate the top of the stack
IAdd	Add the top two elements and push back
IMul	Multiply the top two elements and push back
IBind nm	Bind the value on top of stack to name
IForget	Pop and ignore the binding on the environment

Instances

Instances details

Arbitrary (Instr nm val) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods arbitrary :: Gen (Instr nm val) # shrink :: Instr nm val -> [Instr nm val] #
(SymVal nm, SymVal val) => SymVal (Instr nm val) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV (Instr nm val)) Source # mkSymValInit :: State -> SBV (Instr nm val) -> IO () Source # literal :: Instr nm val -> SBV (Instr nm val) Source # fromCV :: CV -> Instr nm val Source # isConcretely :: SBV (Instr nm val) -> (Instr nm val -> Bool) -> Bool Source # minMaxBound :: Maybe (Instr nm val, Instr nm val) Source # free :: MonadSymbolic m => String -> m (SBV (Instr nm val)) Source # free_ :: MonadSymbolic m => m (SBV (Instr nm val)) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV (Instr nm val)] Source # symbolic :: MonadSymbolic m => String -> m (SBV (Instr nm val)) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV (Instr nm val)] Source # unliteral :: SBV (Instr nm val) -> Maybe (Instr nm val) Source # unlitCV :: SBV (Instr nm val) -> Maybe (Kind, CVal) Source # isConcrete :: SBV (Instr nm val) -> Bool Source # isSymbolic :: SBV (Instr nm val) -> Bool Source #
(HasKind nm, HasKind val) => HasKind (Instr nm val) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods kindOf :: Instr nm val -> Kind Source # hasSign :: Instr nm val -> Bool Source # intSizeOf :: Instr nm val -> Int Source # isBoolean :: Instr nm val -> Bool Source # isBounded :: Instr nm val -> Bool Source # isReal :: Instr nm val -> Bool Source # isFloat :: Instr nm val -> Bool Source # isDouble :: Instr nm val -> Bool Source # isRational :: Instr nm val -> Bool Source # isFP :: Instr nm val -> Bool Source # isUnbounded :: Instr nm val -> Bool Source # isADT :: Instr nm val -> Bool Source # isChar :: Instr nm val -> Bool Source # isString :: Instr nm val -> Bool Source # isList :: Instr nm val -> Bool Source # isSet :: Instr nm val -> Bool Source # isTuple :: Instr nm val -> Bool Source # isArray :: Instr nm val -> Bool Source # isRoundingMode :: Instr nm val -> Bool Source # isUninterpreted :: Instr nm val -> Bool Source # showType :: Instr nm val -> String Source #
(SymVal nm, SymVal val) => HasInductionSchema (Forall ta (Instr nm val) -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Instr nm val) -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT) => HasInductionSchema (Forall ta (Instr nm val) -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Instr nm val) -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

type SInstr nm val = SBV (Instr nm val) Source #

Symbolic version of the type Instr.

Compilation

compile :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SList (Instr nm val) Source #

Convert an expression to a sequence of instructions for our virtual machine.

compileAndRun :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SBV val Source #

Compile and run an expression.

Correctness of the compiler

correctness :: (SymVal nm, SymVal val, Num (SBV val)) => TP (Proof (Forall "expr" (Expr nm val) -> SBool)) Source #

The property we're after is that interpreting an expression is the same as first compiling it to virtual-machine instructions, and then running them.

>>> runTP (correctness @String @Integer)
Inductive lemma: runSeq
  Step: Base                            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Result:                               Q.E.D.
Lemma: runOne                           Q.E.D.
Lemma: runTwo
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Result:                               Q.E.D.
Lemma: runMul                           Q.E.D.
Lemma: measureNonNeg                    Q.E.D.
Inductive lemma (strong): helper
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (7 way case split)
    Step: 1.1.1 (case Var)              Q.E.D.
    Step: 1.1.2                         Q.E.D.
    Step: 1.2.1 (case Con)              Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.2.3                         Q.E.D.
    Step: 1.3.1 (case Sqr)              Q.E.D.
    Step: 1.3.2                         Q.E.D.
    Step: 1.3.3                         Q.E.D.
    Step: 1.3.4                         Q.E.D.
    Step: 1.3.5                         Q.E.D.
    Step: 1.3.6                         Q.E.D.
    Step: 1.3.7                         Q.E.D.
    Step: 1.4.1 (case Inc)              Q.E.D.
    Step: 1.4.2                         Q.E.D.
    Step: 1.4.3                         Q.E.D.
    Step: 1.4.4                         Q.E.D.
    Step: 1.4.5                         Q.E.D.
    Step: 1.4.6                         Q.E.D.
    Step: 1.4.7                         Q.E.D.
    Step: 1.5.1 (case sAdd)             Q.E.D.
    Step: 1.5.2                         Q.E.D.
    Step: 1.5.3                         Q.E.D.
    Step: 1.5.4                         Q.E.D.
    Step: 1.5.5                         Q.E.D.
    Step: 1.5.6                         Q.E.D.
    Step: 1.5.7                         Q.E.D.
    Step: 1.5.8                         Q.E.D.
    Step: 1.5.9                         Q.E.D.
    Step: 1.6.1 (case sMul)             Q.E.D.
    Step: 1.6.2                         Q.E.D.
    Step: 1.6.3                         Q.E.D.
    Step: 1.6.4                         Q.E.D.
    Step: 1.6.5                         Q.E.D.
    Step: 1.6.6                         Q.E.D.
    Step: 1.6.7                         Q.E.D.
    Step: 1.6.8                         Q.E.D.
    Step: 1.6.9                         Q.E.D.
    Step: 1.7.1 (case Let)              Q.E.D.
    Step: 1.7.2                         Q.E.D.
    Step: 1.7.3                         Q.E.D.
    Step: 1.7.4                         Q.E.D.
    Step: 1.7.5                         Q.E.D.
    Step: 1.7.6                         Q.E.D.
    Step: 1.7.7                         Q.E.D.
    Step: 1.7.8                         Q.E.D.
    Step: 1.7.9                         Q.E.D.
    Step: 1.7.10                        Q.E.D.
    Step: 1.7.11                        Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Lemma: correctness
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Result:                               Q.E.D.
[Proven] correctness :: Ɐexpr ∷ (Expr [Char] Integer) → Bool