X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=4319a1c4cff2a44118a19a8b0968cd29d03bd241;hp=bdcf1e65cbd882ad46aaa6891205bee60ed07666;hb=649b9b9ce6db92cc131a1c048c1d9c8719180c58;hpb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index bdcf1e6..4319a1c 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -11,7 +11,8 @@ 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.
@@ -101,7 +102,7 @@ Fixpoint typeToLatexMath (needparens:bool){κ}(t:RawHaskType (fun _ => LatexMath
                                       ; 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 "}")+++
@@ -126,7 +127,7 @@ Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameS
     | 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.
@@ -145,9 +146,9 @@ Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameS
 
 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))
@@ -160,6 +161,7 @@ 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"
@@ -174,7 +176,7 @@ Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
 
 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"
@@ -187,12 +189,13 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"
     | RLet          _ _ _ _ _ _ _     => "Let"
-    | RBindingGroup _ _ _ _ _ _       => "RBindingGroup"
+    | RWhere        _ _ _ _ _ _ _ _   => "Where"
+    | RJoin         _ _ _ _ _ _ _     => "RJoin"
     | 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 :=
@@ -214,9 +217,9 @@ Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
   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
+    | RJoin _ _ _ _ _ _ _ => true
     | _                         => false
   end.
 
@@ -224,5 +227,5 @@ Instance ToLatexMathRule h c : ToLatexMath (Rule h c) :=
   { 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 [])).