ContentsIndex
Core.Defs
Contents
Program and Region
Rules
Monad for user interaction
Conditions
Boxable values
The Goal:
Errors
Description

This module defines the refinement problem we are solving in all generality.

Given the definitions here the goal is to allow construction of Derivation from Core.DerivationTree.

Synopsis
class Syn syn => Prog syn prog | prog -> syn where
mkProg :: MonadI (NodeError syn) m => Code syn -> m prog
getCode :: prog -> Code syn
select :: MonadError' SError m => prog -> Region -> m prog
replace :: MonadError' SError m => prog -> Region -> prog -> m prog
type Code syn = Tree syn
class Eq syn => Syn syn where
arity :: syn -> Arity
isAssoc :: syn -> Bool
data Arity
= Exactly Int
| Any
data Region = Region {
firstNode :: NodePos
lastNode :: NodePos
}
data Rule prog = Rule {
name :: String
desc :: Doc
apply :: (MonadI SError m => prog -> Region -> m (RuleApp prog))
}
data RuleApp prog = RuleApp {
rule :: String
region :: (Maybe Region)
args :: [RuleArg]
origin :: prog
result :: prog
cond :: [Condition]
}
data RuleArg = forall a . Boxable a => RuleArg a
class Monad m => MonadI_ m where
getArgument :: (Boxable a, Parse a) => Doc -> m a
solveCondition :: (ConditionPair cond proof, Parse proof) => cond -> m proof
class (MonadI_ m, MonadError' e m) => MonadI e m
data Condition = forall cond proof . ConditionPair cond proof => Condition cond proof
class (Boxable cond, Boxable proof, Solve cond, Check cond proof) => ConditionPair cond proof
class Solve cond where
solvers :: [Solver cond]
data Solver cond = forall proof . (Boxable proof, Check cond proof) => Solver Doc (cond -> IO proof)
class Check cond proof where
check :: cond -> proof -> IO (Maybe SError)
class (Interfaced a, Storable a) => Boxable a
class (Typeable a, Show a) => Storable a
data Derivation prog = Derivation prog [RuleApp prog]
type SError = String
type NodeError syn = (SError, NodePos, Code syn)
Program and Region
class Syn syn => Prog syn prog | prog -> syn where
The program we are reasoning about with syntax defined by syn.
Methods
mkProg :: MonadI (NodeError syn) m => Code syn -> m prog
getCode :: prog -> Code syn
select :: MonadError' SError m => prog -> Region -> m prog
Select a region withing a program
replace
:: MonadError' SError m
=> progwhole
-> Region
-> progreplacement
-> m prog
Replace a region withing a program
show/hide Instances
type Code syn = Tree syn
Syntax tree of a program
class Eq syn => Syn syn where
Syntactic element of a program. In other words, a node in the syntax tree.
Methods
arity :: syn -> Arity
How many children does this node have?
isAssoc :: syn -> Bool
Does associativity rule hold for this node?
show/hide Instances
data Arity
Number of children of a node in a syntax tree.
Constructors
Exactly Int
AnyAny number
show/hide Instances
data Region

Regions are used to adress a subprogram withing a program. All functions working with regions may assume a correct region, which

  • contains only non-negative values
  • has (length firstNode) == (length lastNode)
  • has firstNode !! i == lastNode !! i for all i < length firstNode

The result p' of select p (Region firstNode lastNode) given a correct region is defined as follows:

  • if firstNode == lastNode then p' is the node addressed by firstNode in p.
  • If last firstNode < last lastNode and the node x adressed by init firstNode in p is associative (see isAssoc) then p' consists of x with children numbered last firstNode to last lastNode.
  • Otherwise an error.

For instance the whole program is given by Region [] [].

Constructors
Region
firstNode :: NodePos
lastNode :: NodePos
show/hide Instances
Read Region
Show Region
Rules
data Rule prog
Constructors
Rule
name :: String
desc :: Doc
apply :: (MonadI SError m => prog -> Region -> m (RuleApp prog))
data RuleApp prog
Result of a rule application
Constructors
RuleApp
rule :: StringThe name of the rule used
region :: (Maybe Region)Nothing for rules that replace the whole program.
args :: [RuleArg]All the arguments passed to the rule
origin :: progThe original program to which the rule was applied.
result :: prog
cond :: [Condition]
show/hide Instances
(Ppr prog, Prog syn prog) => Ppr (RuleApp prog)
Show prog => Show (RuleApp prog)
Typeable prog => Typeable (RuleApp prog)
MonadI_ m => MonadI_ (StateT (RuleApp prog) m)
data RuleArg
Constructors
forall a . Boxable a => RuleArg a
show/hide Instances
Monad for user interaction
class Monad m => MonadI_ m where
Methods
getArgument :: (Boxable a, Parse a) => Doc -> m a
solveCondition :: (ConditionPair cond proof, Parse proof) => cond -> m proof
show/hide Instances
MonadI_ IO
MonadI_ (IFun ITag)
(Error e, MonadI_ m) => MonadI_ (ErrorT e m)
MonadI_ m => MonadI_ (StateT (RuleApp prog) m)
MonadI_ (StateT [RuleArg] IO)
class (MonadI_ m, MonadError' e m) => MonadI e m
show/hide Instances
(MonadI_ m, MonadError' e m) => MonadI e m
Conditions
data Condition
Side conditions produced when applying rules together with their proofs.
Constructors
forall cond proof . ConditionPair cond proof => Condition cond proof
show/hide Instances
class (Boxable cond, Boxable proof, Solve cond, Check cond proof) => ConditionPair cond proof
show/hide Instances
(Boxable cond, Boxable proof, Solve cond, Check cond proof) => ConditionPair cond proof
class Solve cond where
Basic solver. If you want advanced condition solving (for instance depending on the program state), implement it through plugin for the corresponding shell.
Methods
solvers :: [Solver cond]
show/hide Instances
data Solver cond
Constructors
forall proof . (Boxable proof, Check cond proof) => Solver Doc (cond -> IO proof)
class Check cond proof where
Checking should go without user interaction. That means the proof must contain all information to automatically check the condition. Checking might involve reading from an external file (e.g. Isabelle theory), that's why IO.
Methods
check :: cond -> proof -> IO (Maybe SError)
show/hide Instances
Boxable values
class (Interfaced a, Storable a) => Boxable a
show/hide Instances
class (Typeable a, Show a) => Storable a
All objects inside an existential box must belong to this class in order for the box to be storable (serializable).
show/hide Instances
(Typeable a, Show a) => Storable a
The Goal:
data Derivation prog
Constructors
Derivation prog [RuleApp prog]
show/hide Instances
Interfaced (Derivation KProg)
(Show prog, ??? prog) => Show (Derivation prog)
(Typeable prog, ??? prog) => Typeable (Derivation prog)
Check (Refines prog) (Derivation prog)
Errors
type SError = String
type NodeError syn = (SError, NodePos, Code syn)
Error corresponding to some node in the program
Produced by Haddock version 0.8