X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=dedc152bac9bb7df13ba80bbd9514770cbefa61f;hp=d35a87008114aad93dd5cb34c550d515d78904aa;hb=c90b598203ef23bf8d44d6b5b4a5a4b5901039cf;hpb=1c1cdb9014f409248ca96b677503719916b2b477

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index d35a870..dedc152 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -6,6 +6,7 @@ Generalizable All Variables.
 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.
@@ -146,9 +147,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))
@@ -159,23 +160,24 @@ Instance ToLatexMathJudgment : ToLatexMath Judg :=
 
 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"
@@ -188,36 +190,40 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"
     | RLet          _ _ _ _ _ _ _     => "Let"
-    | RJoin _ _ _ _ _ _       => "RJoin"
+    | RCut          _ _ _ _ _ _ _     => "Cut"
+    | RLeft         _ _ _ _ _ _       => "Left"
+    | RRight        _ _ _ _ _ _       => "Right"
+    | RWhere        _ _ _ _ _ _ _ _   => "Where"
+    | RJoin         _ _ _ _ _ _ _     => "RJoin"
     | 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
+    | RJoin _ _ _ _ _ _ _ => true
     | _                         => false
   end.