Require Import Preamble.
Require Import General.
Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import HaskKinds.
Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
match match j return VarNameStoreM LatexMath with
- | mkJudg Γ Δ Σ₁ Σ₂ =>
+ | mkJudg Γ Δ Σ₁ Σ₂ l =>
bind Σ₁' = treeM (mapOptionTree ltypeToLatexMath Σ₁)
- ; bind Σ₂' = treeM (mapOptionTree ltypeToLatexMath Σ₂)
+ ; bind Σ₂' = treeM (mapOptionTree (fun t => ltypeToLatexMath (t@@l)) Σ₂)
; return treeToLatexMath Σ₁' +++ (rawLatexMath "\vdash") +++ treeToLatexMath Σ₂'
end with
varNameStoreM f => fst (f (varNameStore 0 0 0))
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 :=
match r with
- | RArrange _ _ _ _ _ r => nd_uruleToRawLatexMath r
+ | RArrange _ _ _ _ _ _ r => nd_uruleToRawLatexMath r
| RNote _ _ _ _ _ _ => "Note"
| RLit _ _ _ _ => "Lit"
| RVar _ _ _ _ => "Var"
| RAppCo _ _ _ _ _ _ _ _ _ => "AppCo"
| RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
| RApp _ _ _ _ _ _ _ => "App"
- | RLet _ _ _ _ _ _ _ => "Let"
- | RWhere _ _ _ _ _ _ _ _ => "Where"
- | RJoin _ _ _ _ _ _ => "RJoin"
+ | RCut _ _ _ _ _ _ _ _ => "Cut"
+ | RLeft _ _ _ _ _ _ => "Left"
+ | RRight _ _ _ _ _ _ => "Right"
| RLetRec _ _ _ _ _ _ => "LetRec"
| RCase _ _ _ _ _ _ _ _ => "Case"
| RBrak _ _ _ _ _ _ => "Brak"
| REsc _ _ _ _ _ _ => "Esc"
- | RVoid _ _ => "RVoid"
+ | RVoid _ _ _ => "RVoid"
end.
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
+ | RArrange _ _ _ _ _ _ r => nd_hideURule r
+ | RVoid _ _ _ => true
+ | RLeft _ _ _ _ _ _ => true
+ | RRight _ _ _ _ _ _ => true
| _ => false
end.