add an identity production for Arrange

[coq-hetmet.git] / src / HaskProofToLatex.v

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index fb8c2fa..61b358f 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -6,13 +6,13 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
 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.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 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.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskProof.

@@ -102,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
                                       ; 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 "}")+++
                         ; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++
                                  (rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++
                                  (rawLatexMath "}")+++

@@ -127,7 +127,7 @@ Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameS
     | nil => t''
     | lv  => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++
            (fold_left (fun x y => x+++(rawLatexMath ":")+++y)
     | 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.
     end
     end); try apply ConcatenableLatexMath.
     try apply VarNameMonad.

@@ -161,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
   match r with
     | RLeft   _ _ _ r => nd_uruleToRawLatexMath r
     | RRight  _ _ _ r => nd_uruleToRawLatexMath r

+    | RId     _     => "Id"

     | RCanL   _     => "CanL"
     | RCanR   _     => "CanR"
     | RuCanL  _     => "uCanL"
     | RCanL   _     => "CanL"
     | RCanR   _     => "CanR"
     | RuCanL  _     => "uCanL"

@@ -188,12 +189,12 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"
     | RLet          _ _ _ _ _ _ _     => "Let"
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"
     | RLet          _ _ _ _ _ _ _     => "Let"

-    | RBindingGroup _ _ _ _ _ _       => "RBindingGroup"
+    | RJoin _ _ _ _ _ _       => "RJoin"

     | RLetRec       _ _ _ _ _ _       => "LetRec"
     | RCase         _ _ _ _ _ _ _ _   => "Case"
     | RBrak         _ _ _ _ _ _       => "Brak"
     | REsc          _ _ _ _ _ _       => "Esc"
     | 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 :=
 end.
 
 Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=

@@ -216,8 +217,8 @@ Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
   match r with
     | RArrange      _ _ _ _ _ r => nd_hideURule r
 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
   match r with
     | RArrange      _ _ _ _ _ r => nd_hideURule r

-    | REmptyGroup   _ _         => true
-    | RBindingGroup _ _ _ _ _ _ => true
+    | RVoid   _ _         => true
+    | RJoin _ _ _ _ _ _ => true

     | _                         => false
   end.
 
     | _                         => false
   end.
 

@@ -225,5 +226,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) :=
   { 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 [])).