X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=e85bb395429607e55eaf6490bb2acd2843975fe8;hp=fab70fe184e79099de51d9d2570e378b06213222;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=1405918ae8ff55649f864e6fd02b0c0f74fc6607

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index fab70fe..e85bb39 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -6,225 +6,228 @@ Generalizable All Variables.
 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 HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskProof.
 Require Import HaskCoreTypes.
 
-Open Scope string_scope.
-Section HaskProofToLatex.
 
-  Context {TV:Kind -> Type}.
-  Context {TVLatex:forall k, ToLatex (TV k)}.
-  Context {freshM:FreshMonad (∀ κ, TV κ)}.
-  Definition FreshM' := FMT freshM.
-  Instance FreshMon' : Monad FreshM' := FMT_Monad freshM.
-  
-  Instance ToLatexTyCon : ToLatex TyCon.
-    admit.
-    Defined.
 
-  Fixpoint typeToLatex (needparens:bool){κ}(t:RawHaskType TV κ) {struct t} : FMT freshM Latex :=
-    match t with
-    | TVar    _ v        => return toLatex v
-    | TCon    tc         => return (latex "\text{\tt{")+=+tc+=+(latex "}}")
-    | TArrow             => return latex "\text{\tt{(->)}}"
-    | TCoerc _ t1 t2   t => bind t1' = typeToLatex false      t1
-                          ; bind t2' = typeToLatex false      t2
-                          ; bind t'  = typeToLatex needparens t
-                          ; return (latex "{(")+=+t1'+=+(latex "{\sim}")+=+
-                                     t2'+=+(latex ")}\Rightarrow{")+=+t'+=+(latex "}")
-    | TApp  _ _  t1 t2   => match t1 with
-                            | TApp _ _ TArrow tx => bind t1' = typeToLatex true tx
-                                                  ; bind t2' = typeToLatex true t2
-                                                  ; let body := t1'+=+(latex "{\rightarrow}")+=+t2'
-                                                    in return if needparens then (latex "(")+=+body+=+(latex ")") else body
-                            | _                  => bind t1' = typeToLatex true t1
-                                                  ; bind t2' = typeToLatex true t2
-                                                  ; let body := t1'+=+(latex " ")+=+t2'
-                                                    in return if needparens then (latex "(")+=+body+=+(latex ")") else body
-                         end
-    | TCode  ec t        => bind ec' = typeToLatex true ec
-                          ; bind t'  = typeToLatex false t
-                          ; return (latex "\code{")+=+ec'+=+(latex "}{")+=+t'+=+(latex "}")
-    | TyFunApp   tfc lt  => bind rest = typeListToLatex false lt
-                          ; return (latex "{\text{\tt{")+=+(sanitizeForLatex (toString tfc))+=+(latex "}}}")+=+
-                                   (*(latex "_{")+=+(latex (toString (tfc:nat)))+=+(latex "}")+=+*)
-                                   (fold_left (fun x y => (latex " \  ")+=+x+=+y)
-                                     rest (latex ""))
-    | TAll   k f         => (*bind alpha = next
-                          ; bind t'    = typeToLatex false (f (alpha k))
-                          ; *)return (latex "(\forall ")(*+=+(@toLatex _ (TVLatex k) (alpha k))*)
-                          +=+(latex "{:}")+=+(kindToLatex k)+=+(latex ")")(*+=+t'*)
-  end
-  with typeListToLatex (needparens:bool){κ}(t:RawHaskTypeList κ) {struct t} : FreshM' (list Latex) :=
+Inductive VarNameStore :=
+  varNameStore : nat -> nat -> nat -> VarNameStore.
+Inductive VarNameStoreM {T} :=
+  varNameStoreM : (VarNameStore -> (T * VarNameStore)) -> VarNameStoreM.
+Implicit Arguments VarNameStoreM [ ].
+
+Open Scope nat_scope.
+Instance VarNameMonad : Monad VarNameStoreM :=
+{ returnM := fun _   x   => varNameStoreM (fun v => (x,v))
+; bindM   := fun _ _ x f =>
+  match x with
+    varNameStoreM xf =>
+  varNameStoreM (fun vns =>
+    match xf vns with
+      (x',vns') => match f x' with
+                     varNameStoreM fx' => fx' vns'
+                   end
+    end) end }.
+
+Definition freshTyVarName : Kind -> VarNameStoreM LatexMath :=
+  fun κ => varNameStoreM (fun vns =>
+    match vns with
+      varNameStore n1 n2 n3 =>
+      let name := (rawLatexMath "\alpha_{")+++toLatexMath (toString n1)+++(rawLatexMath "}")
+        in (name,(varNameStore (S n1) n2 n3))
+    end).
+Definition freshCoVarName : VarNameStoreM LatexMath :=
+  varNameStoreM (fun vns =>
+    match vns with
+      varNameStore n1 n2 n3 =>
+      let name := (rawLatexMath "\gamma_{")+++toLatexMath (toString n2)+++(rawLatexMath "}")
+        in (name,(varNameStore n1 (S n2) n3))
+    end).
+Definition freshValVarName : VarNameStoreM LatexMath :=
+  varNameStoreM (fun vns =>
+    match vns with
+      varNameStore n1 n2 n3 =>
+      let vn := match n3 with
+                  | 0 => "x"
+                  | 1 => "y"
+                  | 2 => "z"
+                  | 3 => "a"
+                  | 4 => "b"
+                  | 5 => "c"
+                  | 6 => "d"
+                  | 7 => "e"
+                  | 8 => "f"
+                  | 9 => "g"
+                  | 10 => "h"
+                  | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++toString x+++"}"
+                end
+      in let name := rawLatexMath ("x_{"+++vn+++"}")
+        in (name,(varNameStore n1 n2 (S n3)))
+    end).
+
+Fixpoint typeToLatexMath (needparens:bool){κ}(t:RawHaskType (fun _ => LatexMath) κ) {struct t} : VarNameStoreM LatexMath :=
+  match t return VarNameStoreM LatexMath with
+  | TVar    _ v        => return toLatexMath v
+  | TCon    tc         => return ((rawLatexMath "\text{\tt{")+++toLatexMath (toString tc)+++(rawLatexMath "}}"))
+  | TArrow             => return rawLatexMath "\text{\tt{(->)}}"
+  | TCoerc _ t1 t2   t => bind t1' = typeToLatexMath false      t1
+                        ; bind t2' = typeToLatexMath false      t2
+                        ; bind t'  = typeToLatexMath needparens t
+                        ; return ((rawLatexMath "{(")+++t1'+++(rawLatexMath "{\sim}")+++
+                                   t2'+++(rawLatexMath ")}\Rightarrow{")+++t'+++(rawLatexMath "}"))
+  | TCode  ec t        => bind ec' = typeToLatexMath true ec
+                        ; bind t'  = typeToLatexMath false t
+                        ; return (rawLatexMath "\code{")+++ec'+++(rawLatexMath "}{")+++t'+++(rawLatexMath "}")
+  | TAll   k f         => bind alpha = freshTyVarName k
+                        ; bind t'    = typeToLatexMath false (f alpha)
+                        ; return (rawLatexMath "(\forall ")+++alpha+++(rawLatexMath "{:}")+++
+                        (kindToLatexMath k)+++(rawLatexMath ")")+++t'
+  | TApp  _ _  t1 t2   => match t1 return VarNameStoreM LatexMath with
+                | TApp _ _ TArrow tx => bind t1' = typeToLatexMath true tx
+                                      ; bind t2' = typeToLatexMath true t2
+                                      ; let body := t1'+++(rawLatexMath "{\rightarrow}")+++t2'
+                                        in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
+                | _                  => bind t1' = typeToLatexMath true t1
+                                      ; bind t2' = typeToLatexMath true t2
+                                      ; let body := t1'+++(rawLatexMath " ")+++t2'
+                                        in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
+                end
+  | TyFunApp   tfc _ _ lt  => bind rest = typeListToRawLatexMath false lt
+                        ; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++
+                                 (rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++
+                                 (rawLatexMath "}")+++
+                                 (fold_left (fun x y => (rawLatexMath " \  ")+++x+++y)
+                                   rest (rawLatexMath ""))
+end
+with typeListToRawLatexMath (needparens:bool){κ}(t:RawHaskTypeList κ) {struct t} : VarNameStoreM (list LatexMath) :=
+match t return VarNameStoreM (list LatexMath) with
+| TyFunApp_nil                 => return nil
+| TyFunApp_cons  κ kl rhk rhkl => bind r  = typeToLatexMath needparens rhk
+                                ; bind rl = typeListToRawLatexMath needparens rhkl
+                                ; return (r::rl)
+end.
+
+Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameStoreM LatexMath.
+  refine (
   match t with
-  | TyFunApp_nil                 => return nil
-  | TyFunApp_cons  κ kl rhk rhkl => bind r  = typeToLatex needparens rhk
-                                  ; bind rl = typeListToLatex needparens rhkl
-                                  ; return (r::rl)
-  end.
-(*
-  Definition ltypeToLatex {Γ:TypeEnv}{κ}(t:RawHaskType TV κ)(lev:list nat) : FreshM' Latex :=
-    match lev with
-      | nil => typeToLatex false t
-      | lv  => bind t' = typeToLatex true t
-             ; 
-        (latex "{")
-        +=+
-        
-        +=+
-        (latex "}^{")
-        +=+
-        (fold_left (fun x y => x+=+":"+=+y) (map tyvar2greek lv) "")+=+"}"
-    end.
-
-  Open Scope nat_scope.
-  Definition var2string (n:nat) :=
-    match n with
-      | 0 => "x"
-      | 1 => "y"
-      | 2 => "z"
-      | 3 => "a"
-      | 4 => "b"
-      | 5 => "c"
-      | 6 => "d"
-      | 7 => "e"
-      | 8 => "f"
-      | 9 => "g"
-      | 10 => "h"
-      | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++x+++"}"
-    end.
-  Close Scope nat_scope.
-
-  Definition covar2greek (n:nat) :=
-    "{\gamma_{"+++n+++"}}".
-
-  Fixpoint enumerate' (n:nat){T:Type}(l:list T) : list (nat * T) :=
-    match l with
-      | nil    => nil
-      | (a::b) => (n,a)::(enumerate' (S n) b)
-    end.
-
-  Definition enumerate {T:Type}(l:list T) := enumerate' O l.
+    t' @@ lev =>
+    bind ite = _ ;
+    bind t'' = typeToLatexMath false (t' (fun _ => LatexMath) ite) ;
+    return match lev with
+    | nil => t''
+    | lv  => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++
+           (fold_left (fun x y => x+++(rawLatexMath ":")+++y)
+             (map (fun l:HaskTyVar Γ _ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
+    end
+    end); try apply ConcatenableLatexMath.
+    try apply VarNameMonad.
+    clear t t' lev κ.
+    induction Γ.
+    apply (return INil).
+    refine (bind tv' = freshTyVarName a ; _).
+    apply VarNameMonad.
+    refine (bind IHΓ' = IHΓ ; return _).
+    apply VarNameMonad.
+    apply ICons.
+    apply tv'.
+    apply IHΓ'.
+    apply VarNameMonad.
+    Defined.
 
-  Fixpoint count (n:nat) : vec nat n :=
-  match n with
-    | O    => vec_nil
-    | S n' => n':::(count n')
+Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
+  match match j return VarNameStoreM LatexMath with
+    | mkJudg Γ Δ Σ₁ Σ₂ l =>
+          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))
   end.
 
-  Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
-  match lk as LK return IList _ _ LK with
-    | nil    => INil
-    | h::t   => n::::(count' t (S n))
+Instance ToLatexMathJudgment : ToLatexMath Judg :=
+  { toLatexMath := judgmentToRawLatexMath }.
+
+Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
+  match r with
+    | 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.
 
-  Definition InstantiatedTypeEnvString     Γ   : @InstantiatedTypeEnv     (fun _ => nat) Γ := count' Γ O.
-  Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv (fun _ => nat) nat Γ Δ  := count (length Δ).
-  Definition judgmentToLatex (j:Judg) : string :=
-      match j with
-        | mkJudg Γ Δ  a b =>
-          let Γ' := InstantiatedTypeEnvString Γ in
-          let Δ' := InstantiatedCoercionEnvString Γ Δ in
-          let lt2l := fun nt:nat*(LeveledHaskType Γ ★) => 
-            let (n,lt) := nt in
-              match lt with
-                t @@ l =>
-                (var2string n)+++"{:}"+++(@ltypeToLatex Γ _ (t (fun _ => nat) Γ')
-                  (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
-              end in
-          let lt2l' := fun lt:(LeveledHaskType Γ ★) => 
-              match lt with
-                t @@ l =>
-                (@ltypeToLatex Γ _ (t (fun _ => nat) Γ')
-                  (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
-              end in
-          (listToLatex "" lt2l "\ ,\ " (enumerate (leaves a)))
-          +++" \ \vdash_e\  "(*+++"e{:}"*)
-          +++(listToLatex "" lt2l' "\ ,\ " (leaves b))
-      end.
-
-  Definition j2l (j2j:Judg -> Judg) jt :=
-    @judgmentsToLatex Judg judgmentToLatex (mapOptionTree j2j jt).
-
-  Fixpoint nd_uruleToLatex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
-    match r with
-      | RLeft   _ _ _ r => nd_uruleToLatex r
-      | RRight  _ _ _ r => nd_uruleToLatex r
-      | RCanL   _ _     => "CanL"
-      | RCanR   _ _     => "CanR"
-      | RuCanL  _ _     => "uCanL"
-      | RuCanR  _ _     => "uCanR"
-      | RAssoc  _ _ _ _ => "Assoc"
-      | RCossa  _ _ _ _ => "Cossa"
-      | RExch   _ _ _   => "Exch"
-      | RWeak   _ _     => "Weak"
-      | RCont   _ _     => "Cont"
-    end.
-
-  Fixpoint nd_ruleToLatex {h}{c}(r:Rule h c) : string :=
-    match r with
-      | RURule        _ _ _ _ r         => nd_uruleToLatex r
-      | RNote         _ _ _ _ _ _       => "Note"
-      | RLit          _ _ _ _           => "Lit"
-      | RVar          _ _ _ _           => "Var"
-      | RGlobal       _ _ _ _ _         => "Global"
-      | RLam          _ _ _ _ _ _       => "Abs"
-      | RCast         _ _ _ _ _ _ _     => "Cast"
-      | RAbsT         _ _ _ _ _ _       => "AbsT"
-      | RAppT         _ _ _ _ _ _ _     => "AppT"
-      | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
-      | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
-      | RApp          _ _ _ _ _ _ _     => "App"
-      | RLet          _ _ _ _ _ _ _     => "Let"
-      | RBindingGroup _ _ _ _ _ _       => "RBindingGroup"
-      | RLetRec       _ _ _ _ _ _       => "LetRec"
-      | RCase         _ _ _ _ _ _ _ _   => "Case"
-      | RBrak         _ _ _ _ _ _       => "Brak"
-      | REsc          _ _ _ _ _ _       => "Esc"
-      | REmptyGroup   _ _               => "REmptyGroup"
+Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
+  match r with
+    | RArrange      _ _ _ _ _ _ r     => nd_uruleToRawLatexMath r
+    | RNote         _ _ _ _ _ _       => "Note"
+    | RLit          _ _ _ _           => "Lit"
+    | RVar          _ _ _ _           => "Var"
+    | RGlobal       _ _ _ _ _         => "Global"
+    | RLam          _ _ _ _ _ _       => "Abs"
+    | RCast         _ _ _ _ _ _ _     => "Cast"
+    | RAbsT         _ _ _ _ _ _ _     => "AbsT"
+    | RAppT         _ _ _ _ _ _ _     => "AppT"
+    | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
+    | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
+    | RApp          _ _ _ _ _ _ _     => "App"
+    | RCut          _ _ _ _ _ _ _ _   => "Cut"
+    | RLeft         _ _ _ _ _ _       => "Left"
+    | RRight        _ _ _ _ _ _       => "Right"
+    | RLetRec       _ _ _ _ _ _       => "LetRec"
+    | RCase         _ _ _ _ _ _ _ _   => "Case"
+    | RBrak         _ _ _ _ _ _       => "Brak"
+    | REsc          _ _ _ _ _ _       => "Esc"
+    | RVoid         _ _ _             => "RVoid"
+end.
+
+Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
+  match r with
+    | 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
+    | RLeft _ _ _ _  _ _         => true
+    | RRight _  _ _ _ _ _        => true
+    | _                         => false
   end.
 
-  Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ 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
-    end.
-  Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
-    match r with
-      | RURule        _ _ _ _ r   => nd_hideURule r
-      | REmptyGroup   _ _         => true
-      | RBindingGroup _ _ _ _ _ _ => true
-      | _                         => false
-    end.
-  *)
-
-End HaskProofToLatex.
+Instance ToLatexMathRule h c : ToLatexMath (Rule h c) :=
+  { toLatexMath := fun r => rawLatexMath (@nd_ruleToRawLatexMath h c r) }.
 
-(*
-Definition nd_ml_toLatex {c}(pf:@ND _ Rule [] c) :=
-  @SCND_toLatex _ _
-      judgmentToLatex
-      (fun h c r => @nd_ruleToLatex h c r)
-      (fun h c r => @nd_hideRule h c r)
-      _ _ (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).
-*)
\ No newline at end of file
+Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) :=
+@SIND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
+  (mkSIND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).