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 HaskCoreLiterals.
  14 Require Import HaskStrongTypes.
  15 Require Import HaskStrong.
  16 Require Import HaskProof.
  17 Require Import HaskCoreTypes.
  18
  19 (* escapifies any characters which might cause trouble for LaTeX *)
  20 Variable sanitizeForLatex    : string      -> string.        Extract Inlined Constant sanitizeForLatex      => "sanitizeForLatex".
  21
  22 Open Scope string_scope.
  23 Section ToLatex.
  24
  25   Fixpoint kind2latex (k:Kind) : string :=
  26     match k with
  27     | KindType                     => "\star"
  28     | KindTypeFunction KindType k2 => "\star\Rightarrow "+++kind2latex k2
  29     | KindTypeFunction k1 k2       => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
  30     | KindUnliftedType             => "\text{\tt{\#}}"
  31     | KindUnboxedTuple             => "\text{\tt{(\#)}}"
  32     | KindArgType                  => "\text{\tt{?}}"
  33     | KindOpenType                 => "\text{\tt{?}}"
  34     end.
  35
  36   Open Scope nat_scope.
  37   Definition var2string (n:nat) :=
  38     match n with
  39       | 0 => "x"
  40       | 1 => "y"
  41       | 2 => "z"
  42       | 3 => "a"
  43       | 4 => "b"
  44       | 5 => "c"
  45       | 6 => "d"
  46       | 7 => "e"
  47       | 8 => "f"
  48       | 9 => "g"
  49       | 10 => "h"
  50       | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++(nat2string x)+++"}"
  51     end.
  52   Close Scope nat_scope.
  53
  54   Definition tyvar2greek (n:nat) :=
  55     match n with
  56       | O => "\alpha"
  57       | S O => "\beta"
  58       | S (S O) => "\xi"
  59       | S (S (S n)) => "\alpha_{"+++nat2string n+++"}"
  60     end.
  61
  62   Definition covar2greek (n:nat) :=
  63     "{\gamma_{"+++(nat2string n)+++"}}".
  64
  65   Fixpoint count (n:nat) : vec nat n :=
  66   match n with
  67     | O    => vec_nil
  68     | S n' => n':::(count n')
  69   end.
  70
  71   Fixpoint type2latex (needparens:bool)(n:nat)(t:RawHaskType nat) {struct t} : string :=
  72     match t with
  73     | TVar   v                                => tyvar2greek v
  74     | TCon    tc                              => "\text{\tt{"+++sanitizeForLatex (tyConToString tc) +++"}}"
  75     | TCoerc t1 t2   t                        => "{("+++type2latex false n t1+++"{\sim}"
  76                                                      +++type2latex false n t2+++")}\Rightarrow{"
  77                                                      +++type2latex needparens n t+++"}"
  78     | (TApp (TApp TArrow t1) t2)              =>
  79       (if needparens
  80                             then "("+++(type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)+++")"
  81                             else (type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2))
  82     | TArrow => "\text{\tt{(->)}}"
  83     | TApp   t1 t2                            =>
  84                      if needparens
  85                      then "("+++(type2latex true n t1)+++" "+++(type2latex false n t2)+++")"
  86                      else (type2latex true n t1)+++" "+++(type2latex false n t2)
  87     | TFCApp   tfc lt                         => "{\text{\tt{"+++sanitizeForLatex (tyConToString tfc) +++"}}}"+++
  88                                                  "_{"+++(nat2string n)+++"}"+++
  89                                                  fold_left (fun x y => " \  "+++x+++y)
  90                                                  ((fix type2latex_vec (needparens:bool)(n:nat){m}(lt:vec (RawHaskType nat) m)
  91                                                    : list string :=
  92                                                    match lt with
  93                                                      | vec_nil => nil
  94                                                      | a:::b   => (type2latex needparens n a)::(type2latex_vec needparens n _ b)
  95                                                    end )
  96                                                    false n _ lt) ""
  97     | TAll   k f                              => let alpha := tyvar2greek n
  98                                                  in "(\forall "+++ alpha +++ "{:}"+++ kind2latex k +++")"+++
  99                                                       type2latex false (S n) (f n)
 100     | TCode  ec t                             => "\code{"+++(type2latex true n ec)+++"}{"+++(type2latex false n t)+++"}"
 101     end.
 102
 103   Definition ltype2latex {Γ:TypeEnv}(t:RawHaskType nat)(lev:list nat) : string :=
 104     match lev with
 105       | nil => type2latex false O t
 106       | lv  => "{"+++type2latex true O t+++"}^{"+++(fold_left (fun x y => x+++":"+++y) (map tyvar2greek lv) "")+++"}"
 107     end.
 108
 109   Fixpoint enumerate' (n:nat){T:Type}(l:list T) : list (nat * T) :=
 110     match l with
 111       | nil    => nil
 112       | (a::b) => (n,a)::(enumerate' (S n) b)
 113     end.
 114
 115   Definition enumerate {T:Type}(l:list T) := enumerate' O l.
 116
 117   Definition InstantiatedTypeEnvString Γ : @InstantiatedTypeEnv nat Γ := count (length Γ).
 118   Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv nat nat Γ Δ := count (length Δ).
 119   Definition judgment2latex (j:Judg) : string :=
 120       match j with
 121         | mkJudg Γ Δ  a b =>
 122           let Γ' := InstantiatedTypeEnvString Γ in
 123           let Δ' := InstantiatedCoercionEnvString Γ Δ in
 124           let lt2l := fun nt:nat*(LeveledHaskType Γ) =>
 125             let (n,lt) := nt in
 126               match lt with
 127                 t @@ l =>
 128                 (var2string n)+++"{:}"+++(@ltype2latex Γ (t nat Γ') (map (fun x:HaskTyVar Γ => x nat Γ') l))
 129               end in
 130           let lt2l' := fun lt:(LeveledHaskType Γ) =>
 131               match lt with
 132                 t @@ l =>
 133                 "e{:}"+++(@ltype2latex Γ (t nat Γ') (map (fun x:HaskTyVar Γ => x nat Γ') l))
 134               end in
 135           (list2latex "" lt2l "\ ,\ " (enumerate (leaves a)))
 136           +++" \ \vdash_e\  "(*+++"e{:}"*)
 137           +++(list2latex "" lt2l' "\ ,\ " (leaves b))
 138       end.
 139
 140   Definition j2l (j2j:Judg -> Judg) jt :=
 141     @judgments2latex Judg judgment2latex (mapOptionTree j2j jt).
 142
 143   Fixpoint nd_urule2latex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
 144     match r with
 145       | (RLeft   _ _  c r  ) => nd_urule2latex r
 146       | (RRight   _ _ c r  ) => nd_urule2latex r
 147       | (RCanL   t a       ) => "CanL"
 148       | (RCanR   t a       ) => "CanR"
 149       | (RuCanL  t a       ) => "uCanL"
 150       | (RuCanR  t a       ) => "uCanR"
 151       | (RAssoc  t a b c   ) => "Assoc"
 152       | (RCossa  t a b c   ) => "Cossa"
 153       | (RExch   t a b     ) => "Exch"
 154       | (RWeak   t a       ) => "Weak"
 155       | (RCont   t a       ) => "Cont"
 156     end.
 157
 158   Fixpoint nd_rule2latex {h}{c}(r:Rule h c) : string :=
 159     match r with
 160       | RURule _ _ _ _ r => nd_urule2latex r
 161       | RNote   x n z        => "Note"
 162       | RLit    Γ _ l     _    => "Lit"
 163       | RVar    Γ _ σ         p => "Var"
 164       | RLam    Γ _ Σ tx te   p x => "Abs"
 165       | RCast   Γ _ Σ σ τ γ   p x => "Cast"
 166       | RAbsT   Γ  Σ κ σ a   p    => "AbsT"
 167       | RAppT   Γ _  Σ κ σ τ   p y => "AppT"
 168       | RAppCo  Γ _ Σ  _ σ₁ σ₂ σ γ p  => "AppCo"
 169       | RAbsCo  Γ  Σ κ σ cc σ₁ σ₂ p y q  => "AbsCo"
 170       | RApp    Γ _ Σ₁ Σ₂ tx te p => "App"
 171       | RLet    Γ _ Σ₁ Σ₂ σ₁ σ₂ p => "Let"
 172       | REmptyGroup _ a => "REmptyGroup"
 173       | RBindingGroup _ a b c d e => "RBindingGroup"
 174       | RLetRec Γ _ p lri q  => "LetRec"
 175       | RCase   Σ Γ T κlen κ  ldcd τ  _  => "Case"
 176       | RBrak   Σ _ a b c _ => "Brak"
 177       | REsc   Σ _ a b c _ => "Esc"
 178   end.
 179
 180   Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
 181     match r with
 182       | RLeft  h c ctx r   => nd_hideURule r
 183       | RRight h c ctx r   => nd_hideURule r
 184       | RCanL   t a        => true
 185       | RCanR   t a        => true
 186       | RuCanL  t a        => true
 187       | RuCanR  t a        => true
 188       | RAssoc  t a b c    => true
 189       | RCossa  t a b c    => true
 190       | RExch   t (T_Leaf None) b     => true
 191       | RExch   t a  (T_Leaf None)    => true
 192       | RWeak   t (T_Leaf None)       => true
 193       | RCont   t (T_Leaf None)       => true
 194       | _ => false
 195     end.
 196   Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
 197     match r with
 198       | RURule _ _ _ _ r => nd_hideURule r
 199       | REmptyGroup a _ => true
 200       | RBindingGroup _ _ _ _ _ _  => true
 201       | _ => false
 202     end.
 203 End ToLatex.
 204
 205 Definition nd_ml_toLatex {c}(pf:@ND _ Rule [] c) :=
 206   @SCND_toLatex _ _
 207       judgment2latex
 208       (fun h c r => @nd_rule2latex h c r)
 209       (fun h c r => @nd_hideRule h c r)
 210       _ _ (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).