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 HaskGeneral.
  13 Require Import HaskLiterals.
  14 Require Import HaskStrongTypes.
  15 Require Import HaskStrong.
  16 Require Import HaskProof.
  17
  18 (* escapifies any characters which might cause trouble for LaTeX *)
  19 Variable sanitizeForLatex    : string      -> string.        Extract Inlined Constant sanitizeForLatex      => "sanitizeForLatex".
  20 Variable nat2string          : nat         -> string.        Extract Inlined Constant nat2string            => "nat2string".
  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 κ                                => "{\text{\tt{(+>)}}}_{"+++ kind2latex κ +++"}"
  76     | TApp   t1 t2                            =>
  77       match (match t1 with
  78         | TApp (TCon 2 tc) t1' =>
  79           if (tyCon_eq tc ArrowTyCon)
  80             then inl _ (if needparens
  81                             then "("+++(type2latex true n t1')+++"{\rightarrow}"+++(type2latex true n t2)+++")"
  82                             else (type2latex true n t1')+++"{\rightarrow}"+++(type2latex true n t2))
  83             else inr _ tt
  84         | _ => inr _ tt
  85       end) with
  86       | inl  x    => x
  87       | _         => if needparens
  88                      then "("+++(type2latex true n t1)+++" "+++(type2latex false n t2)+++")"
  89                      else (type2latex true n t1)+++" "+++(type2latex false n t2)
  90       end
  91     | TFCApp n tfc lt                         => "{\text{\tt{"+++sanitizeForLatex (tyFunToString _ tfc) +++"}}}"+++
  92                                                  "_{"+++(nat2string n)+++"}"+++
  93                                                  fold_left (fun x y => " \  "+++x+++y)
  94                                                  ((fix type2latex_vec (needparens:bool)(n:nat){m}(lt:vec (RawHaskType nat) m)
  95                                                    : list string :=
  96                                                    match lt with
  97                                                      | vec_nil => nil
  98                                                      | a:::b   => (type2latex needparens n a)::(type2latex_vec needparens n _ b)
  99                                                    end )
 100                                                    false n _ lt) ""
 101     | TAll   k f                              => let alpha := tyvar2greek n
 102                                                  in "(\forall "+++ alpha +++ "{:}"+++ kind2latex k +++")"+++
 103                                                       type2latex false (S n) (f n)
 104     | TCode  ec t                             => "\code{"+++(type2latex true n ec)+++"}{"+++(type2latex false n t)+++"}"
 105     end.
 106
 107   Definition ltype2latex {Γ:TypeEnv}(t:RawHaskType nat)(lev:list nat) : string :=
 108     match lev with
 109       | nil => type2latex false O t
 110       | lv  => "{"+++type2latex true O t+++"}^{"+++(fold_left (fun x y => x+++":"+++y) (map tyvar2greek lv) "")+++"}"
 111     end.
 112
 113   Fixpoint enumerate' (n:nat){T:Type}(l:list T) : list (nat * T) :=
 114     match l with
 115       | nil    => nil
 116       | (a::b) => (n,a)::(enumerate' (S n) b)
 117     end.
 118
 119   Definition enumerate {T:Type}(l:list T) := enumerate' O l.
 120
 121   Definition InstantiatedTypeEnvString Γ : @InstantiatedTypeEnv nat Γ := count (length Γ).
 122   Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv nat nat Γ Δ := count (length Δ).
 123   Definition judgment2latex (j:Judg) : string :=
 124       match j with
 125         | mkJudg Γ Δ  a b =>
 126           let Γ' := InstantiatedTypeEnvString Γ in
 127           let Δ' := InstantiatedCoercionEnvString Γ Δ in
 128           let lt2l := fun nt:nat*(LeveledHaskType Γ) =>
 129             let (n,lt) := nt in
 130               match lt with
 131                 t @@ l =>
 132                 (var2string n)+++"{:}"+++(@ltype2latex Γ (t nat Γ') (map (fun x:HaskTyVar Γ => x nat Γ') l))
 133               end in
 134           let lt2l' := fun lt:(LeveledHaskType Γ) =>
 135               match lt with
 136                 t @@ l =>
 137                 "e{:}"+++(@ltype2latex Γ (t nat Γ') (map (fun x:HaskTyVar Γ => x nat Γ') l))
 138               end in
 139           (list2latex "" lt2l "\ ,\ " (enumerate (leaves a)))
 140           +++" \ \vdash_e\  "(*+++"e{:}"*)
 141           +++(list2latex "" lt2l' "\ ,\ " (leaves b))
 142       end.
 143
 144   Definition j2l (j2j:Judg -> Judg) jt :=
 145     @judgments2latex Judg judgment2latex (mapOptionTree j2j jt).
 146
 147   Fixpoint nd_urule2latex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
 148     match r with
 149       | (RLeft   _ _  c r  ) => nd_urule2latex r
 150       | (RRight   _ _ c r  ) => nd_urule2latex r
 151       | (RCanL   t a       ) => "CanL"
 152       | (RCanR   t a       ) => "CanR"
 153       | (RuCanL  t a       ) => "uCanL"
 154       | (RuCanR  t a       ) => "uCanR"
 155       | (RAssoc  t a b c   ) => "Assoc"
 156       | (RCossa  t a b c   ) => "Cossa"
 157       | (RExch   t a b     ) => "Exch"
 158       | (RWeak   t a       ) => "Weak"
 159       | (RCont   t a       ) => "Cont"
 160     end.
 161
 162   Fixpoint nd_rule2latex {h}{c}(r:Rule h c) : string :=
 163     match r with
 164       | RURule _ _ _ _ r => nd_urule2latex r
 165       | RNote   x n z        => "Note"
 166       | RLit    Γ _ l     _    => "Lit"
 167       | RVar    Γ _ σ         p => "Var"
 168       | RLam    Γ _ Σ tx te   p x => "Abs"
 169       | RCast   Γ _ Σ σ τ γ   p x => "Cast"
 170       | RAbsT   Γ  Σ κ σ a   p    => "AbsT"
 171       | RAppT   Γ _  Σ κ σ τ   p y => "AppT"
 172       | RAppCo  Γ _ Σ κ _ σ₁ σ₂ σ γ p  => "AppCo"
 173       | RAbsCo  Γ  Σ κ σ cc σ₁ σ₂ p y q  => "AbsCo"
 174       | RApp    Γ _ Σ₁ Σ₂ tx te p => "App"
 175       | RLet    Γ _ Σ₁ Σ₂ σ₁ σ₂ p => "Let"
 176       | REmptyGroup _ a => "REmptyGroup"
 177       | RBindingGroup _ a b c d e => "RBindingGroup"
 178       | RLetRec Γ _ p lri q  => "LetRec"
 179       | RCase   Σ Γ T κlen κ  ldcd τ  _ _ => "Case"
 180       | RBrak   Σ _ a b c _ => "Brak"
 181       | REsc   Σ _ a b c _ => "Esc"
 182   end.
 183
 184   Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
 185     match r with
 186       | RLeft  h c ctx r   => nd_hideURule r
 187       | RRight h c ctx r   => nd_hideURule r
 188       | RCanL   t a        => true
 189       | RCanR   t a        => true
 190       | RuCanL  t a        => true
 191       | RuCanR  t a        => true
 192       | RAssoc  t a b c    => true
 193       | RCossa  t a b c    => true
 194       | RExch   t (T_Leaf None) b     => true
 195       | RExch   t a  (T_Leaf None)    => true
 196       | RWeak   t (T_Leaf None)       => true
 197       | RCont   t (T_Leaf None)       => true
 198       | _ => false
 199     end.
 200   Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
 201     match r with
 202       | RURule _ _ _ _ r => nd_hideURule r
 203       | REmptyGroup a _ => true
 204       | RBindingGroup _ _ _ _ _ _  => true
 205       | _ => false
 206     end.
 207 End ToLatex.
 208
 209 Definition nd_ml_toLatex {c}(pf:@ND _ Rule [] c) :=
 210   @SCND_toLatex _ _
 211       judgment2latex
 212       (fun h c r => @nd_rule2latex h c r)
 213       (fun h c r => @nd_hideRule h c r)
 214       _ _ (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).