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