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