X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=4773effcb4e04424caeef1ac2d8ed7b188694634;hp=39dd8ba1d28d479b6321b09adb30f8e266d22907;hb=6ef9f270b138fc7aab48013d55a8192ff022c0f1;hpb=97552c1a6dfb32098d4491951929ab1d4aca96a0

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 39dd8ba..4773eff 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -6,7 +6,6 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
-Require Import NaturalDeductionToLatex.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
@@ -157,24 +156,25 @@ Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
 Instance ToLatexMathJudgment : ToLatexMath Judg :=
   { toLatexMath := judgmentToRawLatexMath }.
 
-Fixpoint nd_uruleToRawLatexMath {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
+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"
+    | 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 *)
   end.
 
 Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
   match r with
-    | RURule        _ _ _ _ r         => nd_uruleToRawLatexMath r
+    | RArrange      _ _ _ _ _ r       => nd_uruleToRawLatexMath r
     | RNote         _ _ _ _ _ _       => "Note"
     | RLit          _ _ _ _           => "Lit"
     | RVar          _ _ _ _           => "Var"
@@ -187,35 +187,36 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"
     | RLet          _ _ _ _ _ _ _     => "Let"
-    | RBindingGroup _ _ _ _ _ _       => "RBindingGroup"
+    | RJoin _ _ _ _ _ _       => "RJoin"
     | RLetRec       _ _ _ _ _ _       => "LetRec"
     | RCase         _ _ _ _ _ _ _ _   => "Case"
     | RBrak         _ _ _ _ _ _       => "Brak"
     | REsc          _ _ _ _ _ _       => "Esc"
-    | REmptyGroup   _ _               => "REmptyGroup"
+    | RVoid   _ _               => "RVoid"
 end.
 
-Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
+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
-    | _                             => false
+    | 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 *)
+    | _                           => false
   end.
 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
   match r with
-    | RURule        _ _ _ _ r   => nd_hideURule r
-    | REmptyGroup   _ _         => true
-    | RBindingGroup _ _ _ _ _ _ => true
+    | RArrange      _ _ _ _ _ r => nd_hideURule r
+    | RVoid   _ _         => true
+    | RJoin _ _ _ _ _ _ => true
     | _                         => false
   end.
 
@@ -223,5 +224,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 [])).