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