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.
Require Import HaskWeakVars.
Require Import HaskWeakTypes.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskStrongTypes.
Require Import HaskStrong.
Require Import HaskProof.
; let body := t1'+++(rawLatexMath " ")+++t2'
in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
end
- | TyFunApp tfc lt => bind rest = typeListToRawLatexMath false lt
+ | TyFunApp tfc _ _ lt => bind rest = typeListToRawLatexMath false lt
; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++
(rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++
(rawLatexMath "}")+++
| nil => t''
| lv => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++
(fold_left (fun x y => x+++(rawLatexMath ":")+++y)
- (map (fun l:HaskTyVar Γ ★ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
+ (map (fun l:HaskTyVar Γ _ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
end
end); try apply ConcatenableLatexMath.
try apply VarNameMonad.
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
- | 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"
- | RBindingGroup _ _ _ _ _ _ => "RBindingGroup"
+ | RCut _ _ _ _ _ _ _ _ => "Cut"
+ | RLeft _ _ _ _ _ _ => "Left"
+ | RRight _ _ _ _ _ _ => "Right"
| RLetRec _ _ _ _ _ _ => "LetRec"
| RCase _ _ _ _ _ _ _ _ => "Case"
| RBrak _ _ _ _ _ _ => "Brak"
| REsc _ _ _ _ _ _ => "Esc"
- | REmptyGroup _ _ => "REmptyGroup"
+ | 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
- | REmptyGroup _ _ => true
- | RBindingGroup _ _ _ _ _ _ => true
+ | RArrange _ _ _ _ _ _ r => nd_hideURule r
+ | RVoid _ _ _ => true
+ | RLeft _ _ _ _ _ _ => true
+ | RRight _ _ _ _ _ _ => true
| _ => false
end.
{ toLatexMath := fun r => rawLatexMath (@nd_ruleToRawLatexMath h c r) }.
Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) :=
-@SCND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
- (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).
+@SIND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
+ (mkSIND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).