remove RLet and RWhere

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

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 39dd8ba..716a983 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -6,13 +6,14 @@ 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 NaturalDeductionContext.

 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 +103,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 +128,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.

@@ -146,9 +147,9 @@ Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameS
 
 Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
   match match j return VarNameStoreM LatexMath with
 
 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 ltypeToLatexMath Σ₂)
+        ; bind Σ₂' = treeM (mapOptionTree (fun t => ltypeToLatexMath (t@@l)) Σ₂)

         ; return treeToLatexMath Σ₁' +++ (rawLatexMath "\vdash") +++ treeToLatexMath Σ₂'
   end with
     varNameStoreM f => fst (f (varNameStore 0 0 0))
         ; return treeToLatexMath Σ₁' +++ (rawLatexMath "\vdash") +++ treeToLatexMath Σ₂'
   end with
     varNameStoreM f => fst (f (varNameStore 0 0 0))

@@ -157,24 +158,26 @@ Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
 Instance ToLatexMathJudgment : ToLatexMath Judg :=
   { toLatexMath := judgmentToRawLatexMath }.
 
 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
   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"
+    | 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
   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"
     | RNote         _ _ _ _ _ _       => "Note"
     | RLit          _ _ _ _           => "Lit"
     | RVar          _ _ _ _           => "Var"

@@ -186,36 +189,39 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"
     | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"

-    | RLet          _ _ _ _ _ _ _     => "Let"
-    | RBindingGroup _ _ _ _ _ _       => "RBindingGroup"
+    | RCut          _ _ _ _ _ _ _ _   => "Cut"
+    | RLeft         _ _ _ _ _ _       => "Left"
+    | RRight        _ _ _ _ _ _       => "Right"

     | RLetRec       _ _ _ _ _ _       => "LetRec"
     | RCase         _ _ _ _ _ _ _ _   => "Case"
     | RBrak         _ _ _ _ _ _       => "Brak"
     | REsc          _ _ _ _ _ _       => "Esc"
     | RLetRec       _ _ _ _ _ _       => "LetRec"
     | RCase         _ _ _ _ _ _ _ _   => "Case"
     | RBrak         _ _ _ _ _ _       => "Brak"
     | REsc          _ _ _ _ _ _       => "Esc"

-    | REmptyGroup   _ _               => "REmptyGroup"
+    | RVoid         _ _ _             => "RVoid"

 end.
 
 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
   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
+    | 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
   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
+    | RLeft _ _ _ _  _ _         => true
+    | RRight _  _ _ _ _ _        => true

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

@@ -223,5 +229,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 [])).