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