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

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index e239205..4773eff 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -6,209 +6,223 @@ 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 HaskGeneral.
-Require Import HaskLiterals.
+Require Import HaskKinds.
+Require Import HaskWeakVars.
+Require Import HaskWeakTypes.
+Require Import HaskLiteralsAndTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskProof.
-
-(* escapifies any characters which might cause trouble for LaTeX *)
-Variable sanitizeForLatex    : string      -> string.        Extract Inlined Constant sanitizeForLatex      => "sanitizeForLatex".
-Variable nat2string          : nat         -> string.        Extract Inlined Constant nat2string            => "nat2string".
-
-Open Scope string_scope.
-Section ToLatex.
-
-  Fixpoint kind2latex (k:Kind) : string :=
-    match k with
-    | KindType                     => "\star"
-    | KindTypeFunction KindType k2 => "\star\Rightarrow "+++kind2latex k2
-    | KindTypeFunction k1 k2       => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
-    | KindUnliftedType             => "\text{\tt{\#}}"
-    | KindUnboxedTuple             => "\text{\tt{(\#)}}"
-    | KindArgType                  => "\text{\tt{?}}"
-    | KindOpenType                 => "\text{\tt{?}}"
-    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_{"+++(nat2string x)+++"}"
-    end.
-  Close Scope nat_scope.
-
-  Definition tyvar2greek (n:nat) :=
-    match n with
-      | O => "\alpha"
-      | S O => "\beta"
-      | S (S O) => "\xi"
-      | S (S (S n)) => "\alpha_{"+++nat2string n+++"}"
-    end.
-
-  Definition covar2greek (n:nat) :=
-    "{\gamma_{"+++(nat2string n)+++"}}".
-
-  Fixpoint count (n:nat) : vec nat n :=
-  match n with
-    | O    => vec_nil
-    | S n' => n':::(count n')
+Require Import HaskCoreTypes.
+
+
+
+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
+    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.
+
+Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
+  match match j return VarNameStoreM LatexMath with
+    | mkJudg Γ Δ Σ₁ Σ₂ =>
+          bind Σ₁' = treeM (mapOptionTree ltypeToLatexMath Σ₁)
+        ; bind Σ₂' = treeM (mapOptionTree ltypeToLatexMath Σ₂)
+        ; return treeToLatexMath Σ₁' +++ (rawLatexMath "\vdash") +++ treeToLatexMath Σ₂'
+  end with
+    varNameStoreM f => fst (f (varNameStore 0 0 0))
   end.
 
-  Fixpoint type2latex (needparens:bool)(n:nat)(t:RawHaskType nat) {struct t} : string :=
-    match t with
-    | TVar   v                                => tyvar2greek v
-    | TCon _  tc                              => "\text{\tt{"+++sanitizeForLatex (tyConToString _ tc) +++"}}"
-    | TCoerc κ                                => "{\text{\tt{(+>)}}}_{"+++ kind2latex κ +++"}"
-    | TApp   t1 t2                            =>
-      match (match t1 with
-        | TApp (TCon 2 tc) t1' => 
-          if (tyCon_eq tc ArrowTyCon)
-            then inl _ (if needparens
-                            then "("+++(type2latex true n t1')+++"{\rightarrow}"+++(type2latex true n t2)+++")"
-                            else (type2latex true n t1')+++"{\rightarrow}"+++(type2latex true n t2))
-            else inr _ tt
-        | _ => inr _ tt
-      end) with
-      | inl  x    => x
-      | _         => if needparens
-                     then "("+++(type2latex true n t1)+++" "+++(type2latex false n t2)+++")"
-                     else (type2latex true n t1)+++" "+++(type2latex false n t2)
-      end
-    | TFCApp n tfc lt                         => "{\text{\tt{"+++sanitizeForLatex (tyFunToString _ tfc) +++"}}}"+++
-                                                 "_{"+++(nat2string n)+++"}"+++
-                                                 fold_left (fun x y => " \  "+++x+++y)
-                                                 ((fix type2latex_vec (needparens:bool)(n:nat){m}(lt:vec (RawHaskType nat) m)
-                                                   : list string :=
-                                                   match lt with
-                                                     | vec_nil => nil
-                                                     | a:::b   => (type2latex needparens n a)::(type2latex_vec needparens n _ b)
-                                                   end )
-                                                   false n _ lt) ""
-    | TAll   k f                              => let alpha := tyvar2greek n
-                                                 in "(\forall "+++ alpha +++ "{:}"+++ kind2latex k +++")"+++
-                                                      type2latex false (S n) (f n)
-    | TCode  ec t                             => "\code{"+++(type2latex true n ec)+++"}{"+++(type2latex false n t)+++"}"
-    end.
-
-  Definition ltype2latex {Γ:TypeEnv}(t:RawHaskType nat)(lev:list nat) : string :=
-    match lev with
-      | nil => type2latex false O t
-      | lv  => "{"+++type2latex true O t+++"}^{"+++(fold_left (fun x y => x+++":"+++y) (map tyvar2greek lv) "")+++"}"
-    end.
-
-  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.
-
-  Definition InstantiatedTypeEnvString Γ : @InstantiatedTypeEnv nat Γ := count (length Γ).
-  Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv nat nat Γ Δ := count (length Δ).
-  Definition judgment2latex (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)+++"{:}"+++(@ltype2latex Γ (t nat Γ') (map (fun x:HaskTyVar Γ => x nat Γ') l))
-              end in
-          let lt2l' := fun lt:(LeveledHaskType Γ) => 
-              match lt with
-                t @@ l =>
-                "e{:}"+++(@ltype2latex Γ (t nat Γ') (map (fun x:HaskTyVar Γ => x nat Γ') l))
-              end in
-          (list2latex "" lt2l "\ ,\ " (enumerate (leaves a)))
-          +++" \ \vdash_e\  "(*+++"e{:}"*)
-          +++(list2latex "" lt2l' "\ ,\ " (leaves b))
-      end.
-
-  Definition j2l (j2j:Judg -> Judg) jt :=
-    @judgments2latex Judg judgment2latex (mapOptionTree j2j jt).
-
-  Fixpoint nd_urule2latex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
-    match r with
-      | (RLeft   _ _  c r  ) => nd_urule2latex r
-      | (RRight   _ _ c r  ) => nd_urule2latex r
-      | (RCanL   t a       ) => "CanL"
-      | (RCanR   t a       ) => "CanR"
-      | (RuCanL  t a       ) => "uCanL"
-      | (RuCanR  t a       ) => "uCanR"
-      | (RAssoc  t a b c   ) => "Assoc"
-      | (RCossa  t a b c   ) => "Cossa"
-      | (RExch   t a b     ) => "Exch"
-      | (RWeak   t a       ) => "Weak"
-      | (RCont   t a       ) => "Cont"
-    end.
+Instance ToLatexMathJudgment : ToLatexMath Judg :=
+  { toLatexMath := judgmentToRawLatexMath }.
+
+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 *)
+  end.
 
-  Fixpoint nd_rule2latex {h}{c}(r:Rule h c) : string :=
-    match r with
-      | RURule _ _ _ _ r => nd_urule2latex r
-      | RNote   x n z        => "Note"
-      | RLit    Γ _ l     _    => "Lit"
-      | RVar    Γ _ σ         p => "Var"
-      | RLam    Γ _ Σ tx te   p x => "Abs"
-      | RCast   Γ _ Σ σ τ γ   p x => "Cast"
-      | RAbsT   Γ  Σ κ σ a   p    => "AbsT"
-      | RAppT   Γ _  Σ κ σ τ   p y => "AppT"
-      | RAppCo  Γ _ Σ κ _ σ₁ σ₂ σ γ p  => "AppCo"
-      | RAbsCo  Γ  Σ κ σ cc σ₁ σ₂ p y q  => "AbsCo"
-      | RApp    Γ _ Σ₁ Σ₂ tx te p => "App"
-      | RLet    Γ _ Σ₁ Σ₂ σ₁ σ₂ p => "Let"
-      | REmptyGroup _ a => "REmptyGroup"
-      | RBindingGroup _ a b c d e => "RBindingGroup"
-      | RLetRec Γ _ p lri q  => "LetRec"
-      | RCase   Σ Γ T κlen κ  ldcd τ  _ _ => "Case"
-      | RBrak   Σ _ a b c _ => "Brak"
-      | REsc   Σ _ a b c _ => "Esc"
+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"
+    | RLet          _ _ _ _ _ _ _     => "Let"
+    | RJoin _ _ _ _ _ _       => "RJoin"
+    | 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
+    | 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
+    | RArrange      _ _ _ _ _ r => nd_hideURule r
+    | RVoid   _ _         => true
+    | RJoin _ _ _ _ _ _ => true
+    | _                         => false
   end.
 
-  Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
-    match r with
-      | RLeft  h c ctx r   => nd_hideURule r
-      | RRight h c ctx r   => nd_hideURule r
-      | RCanL   t a        => true
-      | RCanR   t a        => true
-      | RuCanL  t a        => true
-      | RuCanR  t a        => true
-      | RAssoc  t a b c    => true
-      | RCossa  t a b c    => true
-      | RExch   t (T_Leaf None) b     => true
-      | RExch   t a  (T_Leaf None)    => true
-      | RWeak   t (T_Leaf None)       => true
-      | RCont   t (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 a _ => true
-      | RBindingGroup _ _ _ _ _ _  => true
-      | _ => false
-    end.
-End ToLatex.
+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 _ _
-      judgment2latex
-      (fun h c r => @nd_rule2latex h c r)
-      (fun h c r => @nd_hideRule h c r)
-      _ _ (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).
+Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) :=
+@SIND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
+  (mkSIND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).