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