Hello,
I am trying to define a logical calculus using one data
type for the rules. There are three types of rules and each has 0,1 or
2 assumptions (rule, rule1 and rule2 below). I have defined all the
rules as different constructors so the difference between the types
according to 0,1 or 2 assumptions is very weak. I would still like to
be able to group the rules in types according to the number of
assumptions in order to use pattern matching. Is there a simple way to
do that or another way I should implement the data type such that I can
refer to the rules both according to their number of assumptions and
according to their type?
27 data Rule = Axiom {lowseq :: Sequent}
28 | WeakeningL {rule :: Rule, lowseq :: Sequent, foccur :: FormulaOccur}
29 | WeakeningR {rule :: Rule, lowseq :: Sequent, foccur :: FormulaOccur}
30 | ContractionL {rule :: Rule, lowseq :: Sequent, foccur :: FormulaOccur}
31 | ContractionR {rule :: Rule, lowseq :: Sequent, foccur :: FormulaOccur}
32 | PermutationL {rule :: Rule, lowseq :: Sequent}
33 | PermutationR {rule :: Rule, lowseq :: Sequent}
34 | Mix {rule1 :: Rule, rule2 :: Rule, lowseq :: Sequent, foccur :: FormulaOccur}
35 | NotL {rule :: Rule, lowseq :: Sequent, foccur :: FormulaOccur}
36 | NotR {rule :: Rule, lowseq :: Sequent, foccur :: FormulaOccur}
37 | AndL {rule1 :: Rule, rule2 :: Rule, lowseq :: Sequent, foccur :: FormulaOccur}
38 | AndR {rule1 :: Rule, rule2 :: Rule, lowseq :: Sequent, foccur :: FormulaOccur}
39 deriving (Eq, Show)
Thanks,
Tomer