Contents Index

Core.Utils

Contents Operations with regions Writing rules Conditions Proofs

Description

Utility functions for refinement theories.

Synopsis

module Core.DerivationTree class Prog syn prog => HotCodeProg syn prog | prog -> syn where selectCode :: MonadError' SError m => prog -> Region -> m (Code syn) replaceCode :: MonadError' SError m => prog -> Region -> Code syn -> m prog checkRegion :: MonadError' SError m => Region -> m () encodeRegion :: (MonadError' SError m, Syn syn) => Code syn -> Int -> Int -> m Region decodeRegion :: Code syn -> Region -> (Int, Int) foldRegion :: MonadError' SError m => RegionApplyFun a -> a -> Region -> m a type RegionApplyFun a = MonadError' SError m => a -> Region -> m a codeReplaceStep :: Syn syn => RegionApplyFun (Code syn, Code syn -> Code syn) codeSelectStep :: Syn syn => RegionApplyFun (Code syn) class (MonadI SError m, MonadState (RuleApp prog) m) => MonadRule prog m mkRule :: (forall m . MonadRule prog m => m ()) -> String -> Doc -> Rule prog ruleError :: MonadRule prog m => SError -> m a getJustRegion :: MonadRule prog m => m Region getSelectedProg :: (MonadRule prog m, Prog syn prog) => m prog getSelectedCode :: (MonadRule prog m, HotCodeProg syn prog) => m (Code syn) updateCode :: (MonadRule prog m, HotCodeProg syn prog) => Code syn -> m () addCondition :: (MonadRule prog m, Boxable cond, Solve cond) => cond -> m () splitRegion :: (MonadRule prog m, Prog syn prog, Ppr syn) => [Code syn] -> m ([Code syn], [Code syn]) noMatch :: MonadRule prog m => m a data Refines prog = Refines { goal :: prog source :: prog } data NoProof = NoProof data IsabelleFile = IsabelleFile { fileName :: String } region2Doc :: Code prog -> Region -> Doc pos2Doc :: Code prog -> NodePos -> Doc

Documentation

module Core.DerivationTree

Operations with regions

class Prog syn prog => HotCodeProg syn prog | prog -> syn where

Programs that can be manipulated by manipulating their code. Methods selectCode :: MonadError' SError m => prog -> Region -> m (Code syn) The default just does select . getCode, but you can provide a more efficient version. replaceCode :: MonadError' SError m => prog whole -> Region -> Code syn replacement -> m prog Instances HotCodeProg KSyn KProg Syn a => HotCodeProg a (Code a)

checkRegion :: MonadError' SError m => Region -> m ()

Checks whether the region is correct.

encodeRegion :: (MonadError' SError m, Syn syn) => Code syn -> Int -> Int -> m Region

Create region with test for correctness.

decodeRegion :: Code syn -> Region -> (Int, Int)

Assumes the region is correct in respect to the code

foldRegion :: MonadError' SError m => RegionApplyFun a -> a -> Region -> m a

Operations like select and replace are done by recursion. Here we break this recursion down into steps, so that steps are easily combinable. Recursing like in attributed grammar. This is tail-recursion, recursion with backtrack also possible if necessary.

type RegionApplyFun a = MonadError' SError m => a -> Region -> m a

codeReplaceStep :: Syn syn => RegionApplyFun (Code syn, Code syn -> Code syn)

Uses continuation passing

codeSelectStep :: Syn syn => RegionApplyFun (Code syn)

Writing rules

class (MonadI SError m, MonadState (RuleApp prog) m) => MonadRule prog m

Instances (MonadI SError m, MonadState (RuleApp prog) m) => MonadRule prog m

mkRule

:: (forall m . MonadRule prog m => m ()) -> String name -> Doc description -> Rule prog

ruleError :: MonadRule prog m => SError -> m a

getJustRegion :: MonadRule prog m => m Region

getSelectedProg :: (MonadRule prog m, Prog syn prog) => m prog

getSelectedCode :: (MonadRule prog m, HotCodeProg syn prog) => m (Code syn)

updateCode :: (MonadRule prog m, HotCodeProg syn prog) => Code syn -> m ()

addCondition :: (MonadRule prog m, Boxable cond, Solve cond) => cond -> m ()

splitRegion :: (MonadRule prog m, Prog syn prog, Ppr syn) => [Code syn] -> m ([Code syn], [Code syn])

noMatch :: MonadRule prog m => m a

Conditions

data Refines prog

This condition states that the goal refines the source. Constructors Refines goal :: prog source :: prog Instances Interfaced (Refines KProg) Provable (Refines KProg) Show prog => Show (Refines prog) Solve (Refines prog) Typeable prog => Typeable (Refines prog) Check (Refines prog) (Derivation prog)

Proofs

data NoProof

Constructors NoProof Instances Interfaced NoProof Read NoProof Show NoProof Typeable NoProof Check a NoProof

data IsabelleFile

Constructors IsabelleFile fileName :: String Instances Interfaced IsabelleFile Read IsabelleFile Show IsabelleFile Typeable IsabelleFile Check KFormula IsabelleFile Check PFormula IsabelleFile

region2Doc :: Code prog -> Region -> Doc

pos2Doc :: Code prog -> NodePos -> Doc

Produced by Haddock version 0.8