
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

One beginner to another, what about just breaking down and using multiple data declarations, then packing the rules into the outer data type and the misc. parameters into the inner data type?: data RuleBox = Rule0 RuleZero | Rule1 RuleOne Rule | Rule2 RuleTwo Rule Rule data RuleZero = Axiom Sequent data RuleOne = WeakeningL Sequent FormulaOccur | WeakeningR Sequent FormulaOccur | ContractionL ... | Contraction R ... | PermutationL ... | PermutationR ... | NotL ... | NotR ... data RuleTwo = Mix Sequent FormulaOccur | AndL ... | AndR ...

Thanks, I think this is just what I looked for.. I solved it at the end by
having a function to return the type and a list of rules for any rule, but
certainly your solution looks much better.
2009/1/12 David Morse
One beginner to another, what about just breaking down and using multiple data declarations, then packing the rules into the outer data type and the misc. parameters into the inner data type?:
data RuleBox = Rule0 RuleZero | Rule1 RuleOne Rule | Rule2 RuleTwo Rule Rule data RuleZero = Axiom Sequent data RuleOne = WeakeningL Sequent FormulaOccur | WeakeningR Sequent FormulaOccur | ContractionL ... | Contraction R ... | PermutationL ... | PermutationR ... | NotL ... | NotR ... data RuleTwo = Mix Sequent FormulaOccur | AndL ... | AndR ...
participants (2)
-
David Morse
-
Tomer Libal