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 Coq.Strings.String.
  10 Require Import Coq.Lists.List.
  11 Require Import HaskKinds.
  12 Require Import HaskWeakVars.
  13 Require Import HaskWeakTypes.
  14 Require Import HaskLiteralsAndTyCons.
  15 Require Import HaskStrongTypes.
  16 Require Import HaskStrong.
  17 Require Import HaskProof.
  18 Require Import HaskCoreTypes.
  19
  20
  21
  22 Inductive VarNameStore :=
  23   varNameStore : nat -> nat -> nat -> VarNameStore.
  24 Inductive VarNameStoreM {T} :=
  25   varNameStoreM : (VarNameStore -> (T * VarNameStore)) -> VarNameStoreM.
  26 Implicit Arguments VarNameStoreM [ ].
  27
  28 Open Scope nat_scope.
  29 Instance VarNameMonad : Monad VarNameStoreM :=
  30 { returnM := fun _   x   => varNameStoreM (fun v => (x,v))
  31 ; bindM   := fun _ _ x f =>
  32   match x with
  33     varNameStoreM xf =>
  34   varNameStoreM (fun vns =>
  35     match xf vns with
  36       (x',vns') => match f x' with
  37                      varNameStoreM fx' => fx' vns'
  38                    end
  39     end) end }.
  40
  41 Definition freshTyVarName : Kind -> VarNameStoreM LatexMath :=
  42   fun κ => varNameStoreM (fun vns =>
  43     match vns with
  44       varNameStore n1 n2 n3 =>
  45       let name := (rawLatexMath "\alpha_{")+++toLatexMath (toString n1)+++(rawLatexMath "}")
  46         in (name,(varNameStore (S n1) n2 n3))
  47     end).
  48 Definition freshCoVarName : VarNameStoreM LatexMath :=
  49   varNameStoreM (fun vns =>
  50     match vns with
  51       varNameStore n1 n2 n3 =>
  52       let name := (rawLatexMath "\gamma_{")+++toLatexMath (toString n2)+++(rawLatexMath "}")
  53         in (name,(varNameStore n1 (S n2) n3))
  54     end).
  55 Definition freshValVarName : VarNameStoreM LatexMath :=
  56   varNameStoreM (fun vns =>
  57     match vns with
  58       varNameStore n1 n2 n3 =>
  59       let vn := match n3 with
  60                   | 0 => "x"
  61                   | 1 => "y"
  62                   | 2 => "z"
  63                   | 3 => "a"
  64                   | 4 => "b"
  65                   | 5 => "c"
  66                   | 6 => "d"
  67                   | 7 => "e"
  68                   | 8 => "f"
  69                   | 9 => "g"
  70                   | 10 => "h"
  71                   | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++toString x+++"}"
  72                 end
  73       in let name := rawLatexMath ("x_{"+++vn+++"}")
  74         in (name,(varNameStore n1 n2 (S n3)))
  75     end).
  76
  77 Fixpoint typeToLatexMath (needparens:bool){κ}(t:RawHaskType (fun _ => LatexMath) κ) {struct t} : VarNameStoreM LatexMath :=
  78   match t return VarNameStoreM LatexMath with
  79   | TVar    _ v        => return toLatexMath v
  80   | TCon    tc         => return ((rawLatexMath "\text{\tt{")+++toLatexMath (toString tc)+++(rawLatexMath "}}"))
  81   | TArrow             => return rawLatexMath "\text{\tt{(->)}}"
  82   | TCoerc _ t1 t2   t => bind t1' = typeToLatexMath false      t1
  83                         ; bind t2' = typeToLatexMath false      t2
  84                         ; bind t'  = typeToLatexMath needparens t
  85                         ; return ((rawLatexMath "{(")+++t1'+++(rawLatexMath "{\sim}")+++
  86                                    t2'+++(rawLatexMath ")}\Rightarrow{")+++t'+++(rawLatexMath "}"))
  87   | TCode  ec t        => bind ec' = typeToLatexMath true ec
  88                         ; bind t'  = typeToLatexMath false t
  89                         ; return (rawLatexMath "\code{")+++ec'+++(rawLatexMath "}{")+++t'+++(rawLatexMath "}")
  90   | TAll   k f         => bind alpha = freshTyVarName k
  91                         ; bind t'    = typeToLatexMath false (f alpha)
  92                         ; return (rawLatexMath "(\forall ")+++alpha+++(rawLatexMath "{:}")+++
  93                         (kindToLatexMath k)+++(rawLatexMath ")")+++t'
  94   | TApp  _ _  t1 t2   => match t1 return VarNameStoreM LatexMath with
  95                 | TApp _ _ TArrow tx => bind t1' = typeToLatexMath true tx
  96                                       ; bind t2' = typeToLatexMath true t2
  97                                       ; let body := t1'+++(rawLatexMath "{\rightarrow}")+++t2'
  98                                         in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
  99                 | _                  => bind t1' = typeToLatexMath true t1
 100                                       ; bind t2' = typeToLatexMath true t2
 101                                       ; let body := t1'+++(rawLatexMath " ")+++t2'
 102                                         in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
 103                 end
 104   | TyFunApp   tfc _ _ lt  => bind rest = typeListToRawLatexMath false lt
 105                         ; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++
 106                                  (rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++
 107                                  (rawLatexMath "}")+++
 108                                  (fold_left (fun x y => (rawLatexMath " \  ")+++x+++y)
 109                                    rest (rawLatexMath ""))
 110 end
 111 with typeListToRawLatexMath (needparens:bool){κ}(t:RawHaskTypeList κ) {struct t} : VarNameStoreM (list LatexMath) :=
 112 match t return VarNameStoreM (list LatexMath) with
 113 | TyFunApp_nil                 => return nil
 114 | TyFunApp_cons  κ kl rhk rhkl => bind r  = typeToLatexMath needparens rhk
 115                                 ; bind rl = typeListToRawLatexMath needparens rhkl
 116                                 ; return (r::rl)
 117 end.
 118
 119 Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameStoreM LatexMath.
 120   refine (
 121   match t with
 122     t' @@ lev =>
 123     bind ite = _ ;
 124     bind t'' = typeToLatexMath false (t' (fun _ => LatexMath) ite) ;
 125     return match lev with
 126     | nil => t''
 127     | lv  => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++
 128            (fold_left (fun x y => x+++(rawLatexMath ":")+++y)
 129              (map (fun l:HaskTyVar Γ _ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
 130     end
 131     end); try apply ConcatenableLatexMath.
 132     try apply VarNameMonad.
 133     clear t t' lev κ.
 134     induction Γ.
 135     apply (return INil).
 136     refine (bind tv' = freshTyVarName a ; _).
 137     apply VarNameMonad.
 138     refine (bind IHΓ' = IHΓ ; return _).
 139     apply VarNameMonad.
 140     apply ICons.
 141     apply tv'.
 142     apply IHΓ'.
 143     apply VarNameMonad.
 144     Defined.
 145
 146 Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
 147   match match j return VarNameStoreM LatexMath with
 148     | mkJudg Γ Δ Σ₁ Σ₂ =>
 149           bind Σ₁' = treeM (mapOptionTree ltypeToLatexMath Σ₁)
 150         ; bind Σ₂' = treeM (mapOptionTree ltypeToLatexMath Σ₂)
 151         ; return treeToLatexMath Σ₁' +++ (rawLatexMath "\vdash") +++ treeToLatexMath Σ₂'
 152   end with
 153     varNameStoreM f => fst (f (varNameStore 0 0 0))
 154   end.
 155
 156 Instance ToLatexMathJudgment : ToLatexMath Judg :=
 157   { toLatexMath := judgmentToRawLatexMath }.
 158
 159 Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
 160   match r with
 161     | RLeft   _ _ _ r => nd_uruleToRawLatexMath r
 162     | RRight  _ _ _ r => nd_uruleToRawLatexMath r
 163     | RCanL   _     => "CanL"
 164     | RCanR   _     => "CanR"
 165     | RuCanL  _     => "uCanL"
 166     | RuCanR  _     => "uCanR"
 167     | RAssoc  _ _ _ => "Assoc"
 168     | RCossa  _ _ _ => "Cossa"
 169     | RExch   _ _   => "Exch"
 170     | RWeak   _     => "Weak"
 171     | RCont   _     => "Cont"
 172     | RComp   _ _ _ _ _  => "Comp"  (* FIXME: do a better job here *)
 173   end.
 174
 175 Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
 176   match r with
 177     | RArrange      _ _ _ _ _ r       => nd_uruleToRawLatexMath r
 178     | RNote         _ _ _ _ _ _       => "Note"
 179     | RLit          _ _ _ _           => "Lit"
 180     | RVar          _ _ _ _           => "Var"
 181     | RGlobal       _ _ _ _ _         => "Global"
 182     | RLam          _ _ _ _ _ _       => "Abs"
 183     | RCast         _ _ _ _ _ _ _     => "Cast"
 184     | RAbsT         _ _ _ _ _ _       => "AbsT"
 185     | RAppT         _ _ _ _ _ _ _     => "AppT"
 186     | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
 187     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
 188     | RApp          _ _ _ _ _ _ _     => "App"
 189     | RLet          _ _ _ _ _ _ _     => "Let"
 190     | RJoin _ _ _ _ _ _       => "RJoin"
 191     | RLetRec       _ _ _ _ _ _       => "LetRec"
 192     | RCase         _ _ _ _ _ _ _ _   => "Case"
 193     | RBrak         _ _ _ _ _ _       => "Brak"
 194     | REsc          _ _ _ _ _ _       => "Esc"
 195     | RVoid   _ _               => "RVoid"
 196 end.
 197
 198 Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
 199   match r with
 200     | RLeft   _ _ _ r             => nd_hideURule r
 201     | RRight  _ _ _ r             => nd_hideURule r
 202     | RCanL   _                   => true
 203     | RCanR   _                   => true
 204     | RuCanL  _                   => true
 205     | RuCanR  _                   => true
 206     | RAssoc  _ _ _               => true
 207     | RCossa  _ _ _               => true
 208     | RExch      (T_Leaf None) b  => true
 209     | RExch   a  (T_Leaf None)    => true
 210     | RWeak      (T_Leaf None)    => true
 211     | RCont      (T_Leaf None)    => true
 212     | RComp   _ _ _ _ _           => false   (* FIXME: do better *)
 213     | _                           => false
 214   end.
 215 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
 216   match r with
 217     | RArrange      _ _ _ _ _ r => nd_hideURule r
 218     | RVoid   _ _         => true
 219     | RJoin _ _ _ _ _ _ => true
 220     | _                         => false
 221   end.
 222
 223 Instance ToLatexMathRule h c : ToLatexMath (Rule h c) :=
 224   { toLatexMath := fun r => rawLatexMath (@nd_ruleToRawLatexMath h c r) }.
 225
 226 Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) :=
 227 @SIND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
 228   (mkSIND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).