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 HaskLiterals.
  15 Require Import HaskTyCons.
  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 Γ Δ Σ₁ Σ₂ l =>
 150           bind Σ₁' = treeM (mapOptionTree ltypeToLatexMath Σ₁)
 151         ; bind Σ₂' = treeM (mapOptionTree (fun t => ltypeToLatexMath (t@@l)) Σ₂)
 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     | RId     _     => "Id"
 165     | RCanL   _     => "CanL"
 166     | RCanR   _     => "CanR"
 167     | RuCanL  _     => "uCanL"
 168     | RuCanR  _     => "uCanR"
 169     | RAssoc  _ _ _ => "Assoc"
 170     | RCossa  _ _ _ => "Cossa"
 171     | RExch   _ _   => "Exch"
 172     | RWeak   _     => "Weak"
 173     | RCont   _     => "Cont"
 174     | RComp   _ _ _ _ _  => "Comp"  (* FIXME: do a better job here *)
 175   end.
 176
 177 Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
 178   match r with
 179     | RArrange      _ _ _ _ _ _ r     => nd_uruleToRawLatexMath r
 180     | RNote         _ _ _ _ _ _       => "Note"
 181     | RLit          _ _ _ _           => "Lit"
 182     | RVar          _ _ _ _           => "Var"
 183     | RGlobal       _ _ _ _ _         => "Global"
 184     | RLam          _ _ _ _ _ _       => "Abs"
 185     | RCast         _ _ _ _ _ _ _     => "Cast"
 186     | RAbsT         _ _ _ _ _ _       => "AbsT"
 187     | RAppT         _ _ _ _ _ _ _     => "AppT"
 188     | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
 189     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
 190     | RApp          _ _ _ _ _ _ _     => "App"
 191     | RLet          _ _ _ _ _ _ _     => "Let"
 192     | RWhere        _ _ _ _ _ _ _ _   => "Where"
 193     | RJoin         _ _ _ _ _ _ _     => "RJoin"
 194     | RLetRec       _ _ _ _ _ _       => "LetRec"
 195     | RCase         _ _ _ _ _ _ _ _   => "Case"
 196     | RBrak         _ _ _ _ _ _       => "Brak"
 197     | REsc          _ _ _ _ _ _       => "Esc"
 198     | RVoid         _ _ _             => "RVoid"
 199 end.
 200
 201 Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
 202   match r with
 203     | RLeft   _ _ _ r             => nd_hideURule r
 204     | RRight  _ _ _ r             => nd_hideURule r
 205     | RCanL   _                   => true
 206     | RCanR   _                   => true
 207     | RuCanL  _                   => true
 208     | RuCanR  _                   => true
 209     | RAssoc  _ _ _               => true
 210     | RCossa  _ _ _               => true
 211     | RExch      (T_Leaf None) b  => true
 212     | RExch   a  (T_Leaf None)    => true
 213     | RWeak      (T_Leaf None)    => true
 214     | RCont      (T_Leaf None)    => true
 215     | RComp   _ _ _ _ _           => false   (* FIXME: do better *)
 216     | _                           => false
 217   end.
 218 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
 219   match r with
 220     | RArrange _    _ _ _ _ _ r => nd_hideURule r
 221     | RVoid _  _ _         => true
 222     | RJoin _ _ _ _ _ _ _ => true
 223     | _                         => false
 224   end.
 225
 226 Instance ToLatexMathRule h c : ToLatexMath (Rule h c) :=
 227   { toLatexMath := fun r => rawLatexMath (@nd_ruleToRawLatexMath h c r) }.
 228
 229 Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) :=
 230 @SIND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
 231   (mkSIND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).