Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
match r with
- | RLeft _ _ _ r => nd_uruleToRawLatexMath r
- | RRight _ _ _ r => nd_uruleToRawLatexMath r
- | RId _ => "Id"
- | RCanL _ => "CanL"
- | RCanR _ => "CanR"
- | RuCanL _ => "uCanL"
- | RuCanR _ => "uCanR"
- | RAssoc _ _ _ => "Assoc"
- | RCossa _ _ _ => "Cossa"
- | RExch _ _ => "Exch"
- | RWeak _ => "Weak"
- | RCont _ => "Cont"
- | RComp _ _ _ _ _ => "Comp" (* FIXME: do a better job here *)
+ | ALeft _ _ _ r => nd_uruleToRawLatexMath r
+ | ARight _ _ _ r => nd_uruleToRawLatexMath r
+ | AId _ => "Id"
+ | ACanL _ => "CanL"
+ | ACanR _ => "CanR"
+ | AuCanL _ => "uCanL"
+ | AuCanR _ => "uCanR"
+ | AAssoc _ _ _ => "Assoc"
+ | AuAssoc _ _ _ => "Cossa"
+ | AExch _ _ => "Exch"
+ | AWeak _ => "Weak"
+ | ACont _ => "Cont"
+ | AComp _ _ _ _ _ => "Comp" (* FIXME: do a better job here *)
end.
Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
| RAppCo _ _ _ _ _ _ _ _ _ => "AppCo"
| RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
| RApp _ _ _ _ _ _ _ => "App"
- | RLet _ _ _ _ _ _ _ => "Let"
- | RWhere _ _ _ _ _ _ _ _ => "Where"
- | RJoin _ _ _ _ _ _ _ => "RJoin"
+ | RCut _ _ _ _ _ _ _ _ => "Cut"
+ | RLeft _ _ _ _ _ _ => "Left"
+ | RRight _ _ _ _ _ _ => "Right"
| RLetRec _ _ _ _ _ _ => "LetRec"
| RCase _ _ _ _ _ _ _ _ => "Case"
| RBrak _ _ _ _ _ _ => "Brak"
Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
match r with
- | RLeft _ _ _ r => nd_hideURule r
- | RRight _ _ _ r => nd_hideURule r
- | RCanL _ => true
- | RCanR _ => true
- | RuCanL _ => true
- | RuCanR _ => true
- | RAssoc _ _ _ => true
- | RCossa _ _ _ => true
- | RExch (T_Leaf None) b => true
- | RExch a (T_Leaf None) => true
- | RWeak (T_Leaf None) => true
- | RCont (T_Leaf None) => true
- | RComp _ _ _ _ _ => false (* FIXME: do better *)
+ | ALeft _ _ _ r => nd_hideURule r
+ | ARight _ _ _ r => nd_hideURule r
+ | ACanL _ => true
+ | ACanR _ => true
+ | AuCanL _ => true
+ | AuCanR _ => true
+ | AAssoc _ _ _ => true
+ | AuAssoc _ _ _ => true
+ | AExch (T_Leaf None) b => true
+ | AExch a (T_Leaf None) => true
+ | AWeak (T_Leaf None) => true
+ | ACont (T_Leaf None) => true
+ | AComp _ _ _ _ _ => false (* FIXME: do better *)
| _ => false
end.
Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
match r with
| RArrange _ _ _ _ _ _ r => nd_hideURule r
| RVoid _ _ _ => true
- | RJoin _ _ _ _ _ _ _ => true
+ | RLeft _ _ _ _ _ _ => true
+ | RRight _ _ _ _ _ _ => true
| _ => false
end.