src/HaskProofToLatex.v

   1 (*********************************************************************************************************************************)
   2 (* HaskProofToLatex: render HaskProof's as LaTeX code using trfrac.sty                                                           *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import NaturalDeduction.
   9 Require Import NaturalDeductionToLatex.
  10 Require Import Coq.Strings.String.
  11 Require Import Coq.Lists.List.
  12 Require Import HaskKinds.
  13 Require Import HaskWeakVars.
  14 Require Import HaskWeakTypes.
  15 Require Import HaskLiteralsAndTyCons.
  16 Require Import HaskStrongTypes.
  17 Require Import HaskStrong.
  18 Require Import HaskProof.
  19 Require Import HaskCoreTypes.
  20
  21 Open Scope string_scope.
  22 Section HaskProofToLatex.
  23
  24   Context {TV:Kind -> Type}.
  25   Context {TVLatex:forall k, ToLatex (TV k)}.
  26   Context {freshM:FreshMonad (∀ κ, TV κ)}.
  27   Definition FreshM' := FMT freshM.
  28   Instance FreshMon' : Monad FreshM' := FMT_Monad freshM.
  29
  30   Instance ToLatexTyCon : ToLatex TyCon.
  31     admit.
  32     Defined.
  33
  34   Fixpoint typeToLatex (needparens:bool){κ}(t:RawHaskType TV κ) {struct t} : FMT freshM Latex :=
  35     match t with
  36     | TVar    _ v        => return toLatex v
  37     | TCon    tc         => return (latex "\text{\tt{")+=+tc+=+(latex "}}")
  38     | TArrow             => return latex "\text{\tt{(->)}}"
  39     | TCoerc _ t1 t2   t => bind t1' = typeToLatex false      t1
  40                           ; bind t2' = typeToLatex false      t2
  41                           ; bind t'  = typeToLatex needparens t
  42                           ; return (latex "{(")+=+t1'+=+(latex "{\sim}")+=+
  43                                      t2'+=+(latex ")}\Rightarrow{")+=+t'+=+(latex "}")
  44     | TApp  _ _  t1 t2   => match t1 with
  45                             | TApp _ _ TArrow tx => bind t1' = typeToLatex true tx
  46                                                   ; bind t2' = typeToLatex true t2
  47                                                   ; let body := t1'+=+(latex "{\rightarrow}")+=+t2'
  48                                                     in return if needparens then (latex "(")+=+body+=+(latex ")") else body
  49                             | _                  => bind t1' = typeToLatex true t1
  50                                                   ; bind t2' = typeToLatex true t2
  51                                                   ; let body := t1'+=+(latex " ")+=+t2'
  52                                                     in return if needparens then (latex "(")+=+body+=+(latex ")") else body
  53                          end
  54     | TCode  ec t        => bind ec' = typeToLatex true ec
  55                           ; bind t'  = typeToLatex false t
  56                           ; return (latex "\code{")+=+ec'+=+(latex "}{")+=+t'+=+(latex "}")
  57     | TyFunApp   tfc lt  => bind rest = typeListToLatex false lt
  58                           ; return (latex "{\text{\tt{")+=+(sanitizeForLatex (toString tfc))+=+(latex "}}}")+=+
  59                                    (*(latex "_{")+=+(latex (toString (tfc:nat)))+=+(latex "}")+=+*)
  60                                    (fold_left (fun x y => (latex " \  ")+=+x+=+y)
  61                                      rest (latex ""))
  62     | TAll   k f         => (*bind alpha = next
  63                           ; bind t'    = typeToLatex false (f (alpha k))
  64                           ; *)return (latex "(\forall ")(*+=+(@toLatex _ (TVLatex k) (alpha k))*)
  65                           +=+(latex "{:}")+=+(kindToLatex k)+=+(latex ")")(*+=+t'*)
  66   end
  67   with typeListToLatex (needparens:bool){κ}(t:RawHaskTypeList κ) {struct t} : FreshM' (list Latex) :=
  68   match t with
  69   | TyFunApp_nil                 => return nil
  70   | TyFunApp_cons  κ kl rhk rhkl => bind r  = typeToLatex needparens rhk
  71                                   ; bind rl = typeListToLatex needparens rhkl
  72                                   ; return (r::rl)
  73   end.
  74 (*
  75   Definition ltypeToLatex {Γ:TypeEnv}{κ}(t:RawHaskType TV κ)(lev:list nat) : FreshM' Latex :=
  76     match lev with
  77       | nil => typeToLatex false t
  78       | lv  => bind t' = typeToLatex true t
  79              ;
  80         (latex "{")
  81         +=+
  82
  83         +=+
  84         (latex "}^{")
  85         +=+
  86         (fold_left (fun x y => x+=+":"+=+y) (map tyvar2greek lv) "")+=+"}"
  87     end.
  88
  89   Open Scope nat_scope.
  90   Definition var2string (n:nat) :=
  91     match n with
  92       | 0 => "x"
  93       | 1 => "y"
  94       | 2 => "z"
  95       | 3 => "a"
  96       | 4 => "b"
  97       | 5 => "c"
  98       | 6 => "d"
  99       | 7 => "e"
 100       | 8 => "f"
 101       | 9 => "g"
 102       | 10 => "h"
 103       | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++x+++"}"
 104     end.
 105   Close Scope nat_scope.
 106
 107   Definition covar2greek (n:nat) :=
 108     "{\gamma_{"+++n+++"}}".
 109
 110   Fixpoint enumerate' (n:nat){T:Type}(l:list T) : list (nat * T) :=
 111     match l with
 112       | nil    => nil
 113       | (a::b) => (n,a)::(enumerate' (S n) b)
 114     end.
 115
 116   Definition enumerate {T:Type}(l:list T) := enumerate' O l.
 117
 118   Fixpoint count (n:nat) : vec nat n :=
 119   match n with
 120     | O    => vec_nil
 121     | S n' => n':::(count n')
 122   end.
 123
 124   Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
 125   match lk as LK return IList _ _ LK with
 126     | nil    => INil
 127     | h::t   => n::::(count' t (S n))
 128   end.
 129
 130   Definition InstantiatedTypeEnvString     Γ   : @InstantiatedTypeEnv     (fun _ => nat) Γ := count' Γ O.
 131   Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv (fun _ => nat) nat Γ Δ  := count (length Δ).
 132   Definition judgmentToLatex (j:Judg) : string :=
 133       match j with
 134         | mkJudg Γ Δ  a b =>
 135           let Γ' := InstantiatedTypeEnvString Γ in
 136           let Δ' := InstantiatedCoercionEnvString Γ Δ in
 137           let lt2l := fun nt:nat*(LeveledHaskType Γ ★) =>
 138             let (n,lt) := nt in
 139               match lt with
 140                 t @@ l =>
 141                 (var2string n)+++"{:}"+++(@ltypeToLatex Γ _ (t (fun _ => nat) Γ')
 142                   (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
 143               end in
 144           let lt2l' := fun lt:(LeveledHaskType Γ ★) =>
 145               match lt with
 146                 t @@ l =>
 147                 (@ltypeToLatex Γ _ (t (fun _ => nat) Γ')
 148                   (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
 149               end in
 150           (listToLatex "" lt2l "\ ,\ " (enumerate (leaves a)))
 151           +++" \ \vdash_e\  "(*+++"e{:}"*)
 152           +++(listToLatex "" lt2l' "\ ,\ " (leaves b))
 153       end.
 154
 155   Definition j2l (j2j:Judg -> Judg) jt :=
 156     @judgmentsToLatex Judg judgmentToLatex (mapOptionTree j2j jt).
 157
 158   Fixpoint nd_uruleToLatex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
 159     match r with
 160       | RLeft   _ _ _ r => nd_uruleToLatex r
 161       | RRight  _ _ _ r => nd_uruleToLatex r
 162       | RCanL   _ _     => "CanL"
 163       | RCanR   _ _     => "CanR"
 164       | RuCanL  _ _     => "uCanL"
 165       | RuCanR  _ _     => "uCanR"
 166       | RAssoc  _ _ _ _ => "Assoc"
 167       | RCossa  _ _ _ _ => "Cossa"
 168       | RExch   _ _ _   => "Exch"
 169       | RWeak   _ _     => "Weak"
 170       | RCont   _ _     => "Cont"
 171     end.
 172
 173   Fixpoint nd_ruleToLatex {h}{c}(r:Rule h c) : string :=
 174     match r with
 175       | RURule        _ _ _ _ r         => nd_uruleToLatex r
 176       | RNote         _ _ _ _ _ _       => "Note"
 177       | RLit          _ _ _ _           => "Lit"
 178       | RVar          _ _ _ _           => "Var"
 179       | RGlobal       _ _ _ _ _         => "Global"
 180       | RLam          _ _ _ _ _ _       => "Abs"
 181       | RCast         _ _ _ _ _ _ _     => "Cast"
 182       | RAbsT         _ _ _ _ _ _       => "AbsT"
 183       | RAppT         _ _ _ _ _ _ _     => "AppT"
 184       | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
 185       | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
 186       | RApp          _ _ _ _ _ _ _     => "App"
 187       | RLet          _ _ _ _ _ _ _     => "Let"
 188       | RBindingGroup _ _ _ _ _ _       => "RBindingGroup"
 189       | RLetRec       _ _ _ _ _ _       => "LetRec"
 190       | RCase         _ _ _ _ _ _ _ _   => "Case"
 191       | RBrak         _ _ _ _ _ _       => "Brak"
 192       | REsc          _ _ _ _ _ _       => "Esc"
 193       | REmptyGroup   _ _               => "REmptyGroup"
 194   end.
 195
 196   Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
 197     match r with
 198       | RLeft   _ _ _ r               => nd_hideURule r
 199       | RRight  _ _ _ r               => nd_hideURule r
 200       | RCanL   _ _                   => true
 201       | RCanR   _ _                   => true
 202       | RuCanL  _ _                   => true
 203       | RuCanR  _ _                   => true
 204       | RAssoc  _ _ _ _               => true
 205       | RCossa  _ _ _ _               => true
 206       | RExch   _    (T_Leaf None) b  => true
 207       | RExch   _ a  (T_Leaf None)    => true
 208       | RWeak   _    (T_Leaf None)    => true
 209       | RCont   _    (T_Leaf None)    => true
 210       | _                             => false
 211     end.
 212   Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
 213     match r with
 214       | RURule        _ _ _ _ r   => nd_hideURule r
 215       | REmptyGroup   _ _         => true
 216       | RBindingGroup _ _ _ _ _ _ => true
 217       | _                         => false
 218     end.
 219   *)
 220
 221 End HaskProofToLatex.
 222
 223 (*
 224 Definition nd_ml_toLatex {c}(pf:@ND _ Rule [] c) :=
 225   @SCND_toLatex _ _
 226       judgmentToLatex
 227       (fun h c r => @nd_ruleToLatex h c r)
 228       (fun h c r => @nd_hideRule h c r)
 229       _ _ (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).
 230 *)